lean_problem_sheets / 2020.logic.logic_video

theorem modus_ponens (P Q : Prop) :

P → (P → Q) → Q

Modus Ponens : if P is true, and P → Q, then Q is true

theorem and.elim' (P Q R : Prop) :

P ∧ Q → (P → Q → R) → R

theorem and.intro' (P Q : Prop) :

P → Q → P ∧ Q