A B
-----
C
and A B
----- (→c)
C
are logically equivalent, the latter just gives you a name to refer to the rule by. Animal%(is-elephant)
if the type is known to only be an elephant. Though this is not used everywhere it could be right now it is part of the system. This means we have room to do things like if-splitting e.g. if is-elephant(x): ...
would be able to treat x as an Animal%(is-elephant)
in the body rather than just an `Animal`.
However, modus ponens is just one of the names for this. I could also call it function elimination. I could call it →e. Or I could not bother giving it a name and just say that this is a rule in my logic call it whatever you want in your head if you so desire.
Things can get complicated, but they aren't always complicated so naming rules isn't strictly necessary.