mathlib documentation

lean_problem_sheets / 2020.logic.logic_lecture_ad_lib

theorem xena.id (P : Prop) :

P → P

The theorem that P ⇒ P

theorem xena.modus_ponens (P Q : Prop) :

P → (P → Q) → Q

theorem xena.trans (P Q R : Prop) :

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

theorem xena.trans' (P Q R : Prop) :

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

theorem xena.imp_not_not (P : Prop) :

P → ¬¬P

theorem xena.not_not (P : Prop) :

¬¬P → P