tutorials 0019/20

Stream: new members

[Sara Fish]

In the text right between 0019 and 0020 in this tutorial (https://github.com/leanprover-community/tutorials), they write

Similarly, given a proof h of P ↔ Q, one can get a proof of P → Q using h.mp
and a proof of Q → P using h.mpr

What do mp and mpr stand for?

[Yakov Pechersky]

modus ponens and modus ponens, reversed

[Sara Fish]

Ah, of course! Thanks.

[Heather Macbeth]

That's funny, I always thought mp was a mnemonic for "implies" :)

[Johan Commelin]

It's true that I don't think I've ever had this terminology used in any of the courses I took...

[Kevin Buzzard]

But you took very few if any logic courses, right?