Lean Bi-implication

Stream: new members

[Rajiv]

I was reading Logic and Proof here.

https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#bi-implication

I found the following - "Lean recognizes the abbreviation iff.mp for iff.elim_left, where “mp” stands for “modus ponens”. Similarly, you can use iff.mpr, for “modus ponens reverse”, instead of iff.elim_right."

Is there a reason why Modes Ponens is mapped to bi-implication elim and not implication elim (or apply)?

[Reid Barton]

Well iff.mp is in the iff namespace, so it is about iff and does not preclude using mp in other namespaces for other things. On the other hand, there is little need for mp for implication, because as you note it is simply application.

[Rajiv]

Thanks @Reid Barton I wanted to make sure I wasn't missing anything subtle.