更新时间:2023-02-17 13:47:08
(p ⇒ q) ⇒ p
((p ⇒ q) ⇒ p) ∨ (p ⇒ p) ; (X ⇒ X) and Or introduction
((p ⇒ q) ∨ p) ⇒ p ; (X ⇒ Z) ∨ (Y ⇒ Z) |- (X ∨ Y ⇒ Z)
((¬p ∨ q) ∨ p) ⇒ p ; (p ⇒ q) ⇔ (¬p ∨ q)
((¬p ∨ p) ∨ q) ⇒ p ; (X ∨ Y) ∨ Z |- (X ∨ Z) ∨ Y
(true ∨ q) ⇒ p ; (¬X ∨ X) ⇔ true
true ⇒ p ; (true ∨ X) ⇔ true
p ; Implication elimination
((p ⇒ q) ⇒ p) ⇒ p ; Implication introduction