Modus ponens
Closed
Theorem & proof
·
modus_ponens.lean
·
✓ verified
1
2
3
import Mathlib theorem modus_ponens {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp
Rewards pledged
No rewards pledged yet.