# List of theorems

List of theorems in general/Intuitionistic_propositional_logic.gh:

(→ p (→ q r))(→ (→ p q) (→ p r))
(→ p q) , (→ q r)(→ p r)
(→ p p)
ImplicationReflexivity Alternate name for the same theorem:
(→ p p)
(→ p (→ q r))(→ q (→ p r))
(→ (→ p q) (→ (→ r p) (→ r q)))
(→ p q)(→ (→ r p) (→ r q))
(→ (→ p q) (→ (→ q r) (→ p r)))
(→ p q)(→ (→ q r) (→ p r))
(→ (→ p (→ q r)) (→ q (→ p r)))
(→ (→ p (→ p q)) (→ p q))
(→ p (→ p q))(→ p q)
(→ p (→ q p))
p(→ q p)
(→ (→ (→ p q) (→ p r)) (→ p (→ q r)))
(→ (→ p q) (→ p r))(→ p (→ q r))
(→ (→ p (→ q r)) (→ (→ p (→ r s)) (→ p (→ q s))))
(→ p (→ q r)) , (→ p (→ r s))(→ p (→ q s))
p , q(∧ p q)
(∧ p q)q
(∧ p q)p
(→ p (→ q (∧ q p)))
(→ (→ p q) (→ (→ p r) (→ p (∧ q r))))
(→ p q) , (→ p r)(→ p (∧ q r))
(→ (→ p (∧ q r)) (∧ (→ p q) (→ p r)))
(→ p (∧ q r))(→ p q)
(→ p (∧ q r))(→ p r)
(→ (→ p (→ q r)) (→ (→ r common) (→ p (→ q common))))
(→ (→ (∧ p q) r) (→ p (→ q r)))
(→ (∧ p q) r)(→ p (→ q r))
(→ P (→ Q R)) , (→ R (→ Q r))(→ P (→ Q r))
(→ (→ p (→ q r)) (→ (∧ p q) r))
(→ p (→ q r))(→ (∧ p q) r)
(→ (∧ (→ p q) (→ q r)) (→ p r))
(→ (∧ (→ p q) (→ p r)) (→ p (∧ q r)))
(→ (∧ p q) (∧ q p))
(∧ p q)(∧ q p)
(→ (→ p q) (→ (∧ p common) q))
(→ (→ p q) (→ (∧ p common) common))
(→ (→ p q) (→ (∧ p common) (∧ q common)))
(→ p q)(→ (∧ p r) (∧ q r))
(→ (∧ (→ p r) (→ q s)) (→ (∧ p q) (∧ r s)))
(→ p r) , (→ q s)(→ (∧ p q) (∧ r s))
(→ (→ p q) (→ (∧ r p) (∧ r q)))
(→ (→ p q) (→ (∧ r p) (∧ q r)))
(→ (→ p q) (→ (∧ p r) (∧ r q)))
(→ p q)(→ (∧ r p) (∧ r q))
(→ p q)(→ (∧ r p) (∧ q r))
(→ p q)(→ (∧ p r) (∧ r q))
(→ (→ (∨ p q) r) (∧ (→ p r) (→ q r)))
(→ p r) , (→ q r)(→ (∨ p q) r)
p(∨ q p)
p(∨ p q)
(→ (∨ p q) r)(→ p r)
(→ (∨ p q) r)(→ q r)
(→ (∨ p q) (∨ q p))
(∨ p q)(∨ q p)
(→ (→ p q) (→ p (∨ common q)))
(→ (→ p q) (→ common (∨ common q)))
(→ (→ p q) (→ (∨ p common) (∨ common q)))
(→ p q)(→ (∨ p r) (∨ r q))
(→ (∧ (→ p r) (→ q s)) (→ (∨ p q) (∨ r s)))
(→ p r) , (→ q s)(→ (∨ p q) (∨ r s))
(→ (→ p q) (→ (∨ r p) (∨ r q)))
(→ (→ p q) (→ (∨ r p) (∨ q r)))
(→ (→ p q) (→ (∨ p r) (∨ q r)))
(→ p q)(→ (∨ r p) (∨ r q))
(→ p q)(→ (∨ r p) (∨ q r))
(→ p q)(→ (∨ p r) (∨ q r))
BiconditionalJust Justification for the definition of biconditional.
(∧ (→ (∧ (→ p q) (→ q p)) (∧ (→ p q) (→ q p))) (→ (∧ (→ p q) (→ q p)) (∧ (→ p q) (→ q p))))
Biconditional The biconditional p ↔ q is defined as (p → q) ∧ (q → p). If we already had biconditional, it would be fairly straightforward to define it using [BiconditionalReflexivity]. But since we don't, what we'll prove instead is the expanded form of that defintion. The defthm mechanism will then match the p ↔ q term against its expansion. This is quite similar to dfbi in metamath's set.mm, [http://us.metamath.org/mpeuni/dfbi.html]
(∧ (→ (↔ p q) (∧ (→ p q) (→ q p))) (→ (∧ (→ p q) (→ q p)) (↔ p q)))
(→ p q) , (→ q p)(↔ p q)
(→ (↔ p q) (→ q p))
(→ (↔ p q) (→ p q))
(↔ p q)(→ q p)
(↔ p q)(→ p q)
(↔ (→ p (→ q r)) (→ (→ p q) (→ p r)))
(↔ (→ p (→ q r)) (→ (∧ p q) r))
(↔ (∧ (→ p q) (→ p r)) (→ p (∧ q r)))
(↔ (∧ (→ p r) (→ q r)) (→ (∨ p q) r))
(↔ p p)
(→ (↔ p q) (↔ q p))
(↔ (↔ p q) (↔ q p))
(↔ p q)(↔ q p)
(→ (∧ (↔ p q) (↔ q r)) (↔ p r))
(↔ p q) , (↔ q r)(↔ p r)
(↔ (↔ p q) (∧ (→ p q) (→ q p)))
(↔ p q)(∧ (→ p q) (→ q p))
(∧ (→ p q) (→ q p))(↔ p q)
(→ p (∧ p p))
(→ (∧ p p) p)
(↔ p (∧ p p))
p(∧ p p)
(∧ p p)p
(↔ (∧ p q) (∧ q p))
(→ (∧ (∧ p q) r) (∧ p (∧ q r)))
(→ (∧ p (∧ q r)) (∧ (∧ p q) r))
(↔ (∧ (∧ p q) r) (∧ p (∧ q r)))
(∧ (∧ p q) r)(∧ p (∧ q r))
(∧ p (∧ q r))(∧ (∧ p q) r)
(→ p (∨ p p))
(→ (∨ p p) p)
(↔ p (∨ p p))
p(∨ p p)
(∨ p p)p
(↔ (∨ p q) (∨ q p))
(→ (∨ (∨ p q) r) (∨ p (∨ q r)))
(→ (∨ p (∨ q r)) (∨ (∨ p q) r))
(↔ (∨ (∨ p q) r) (∨ p (∨ q r)))
(∨ p (∨ q r))(∨ (∨ p q) r)
(∨ (∨ p q) r)(∨ p (∨ q r))
(→ (∧ (∧ p q) (∧ r s)) (∧ (∧ p r) (∧ q s)))
(→ (∧ (↔ p q) (↔ r s)) (↔ (∧ p r) (∧ q s)))
(↔ p q) , (↔ r s)(↔ (∧ p r) (∧ q s))
(→ (∧ (↔ p q) (↔ r s)) (↔ (∨ p r) (∨ q s)))
(↔ p q) , (↔ r s)(↔ (∨ p r) (∨ q s))
(→ (∨ p (∨ p q)) (∨ p q))
(→ (∧ (∨ p q) (∨ p r)) (∨ p (∧ q r)))
(→ (∧ p (∨ q r)) (∨ (∧ p q) (∧ p r)))
(→ (∨ (∧ p q) (∧ p r)) (∧ p (∨ q r)))
(↔ (∧ p (∨ q r)) (∨ (∧ p q) (∧ p r)))
(→ (∨ p (∧ q r)) (∧ (∨ p q) (∨ p r)))
(↔ (∨ p (∧ q r)) (∧ (∨ p q) (∨ p r)))
(↔ (∨ (∧ p q) r) (∧ (∨ p r) (∨ q r)))
(↔ (∧ (∨ p q) r) (∨ (∧ p r) (∧ q r)))
(∨ p (∧ q r))(∧ (∨ p q) (∨ p r))
(∧ (∨ p q) (∨ p r))(∨ p (∧ q r))
(∨ (∧ p q) r)(∧ (∨ p r) (∨ q r))
(∧ (∨ p r) (∨ q r))(∨ (∧ p q) r)
(∧ p (∨ q r))(∨ (∧ p q) (∧ p r))
(∨ (∧ p q) (∧ p r))(∧ p (∨ q r))
(∧ (∨ p q) r)(∨ (∧ p r) (∧ q r))
(∨ (∧ p r) (∧ q r))(∧ (∨ p q) r)
(↔ (→ p q) (→ p (∧ p q)))
(↔ (→ p q) (↔ p (∧ p q)))
(→ q (↔ p (∧ p q)))
(→ (∧ p (→ p q)) q)
(→ (→ p q) (→ (¬ q) (¬ p)))
(→ p q)(→ (¬ q) (¬ p))
(→ (∧ (¬ q) (→ p q)) (¬ p))
(¬ q) , (→ p q)(¬ p)
(→ p (¬ (¬ p)))
p(¬ (¬ p))
(↔ (¬ (¬ (¬ p))) (¬ p))
(¬ (¬ (¬ p)))(¬ p)
(→ (→ p q) (→ (∨ p q) q))
(→ (∧ (¬ p) (∨ p q)) q)
(→ (¬ (∨ p q)) (∧ (¬ p) (¬ q)))
(→ (∨ (¬ p) (¬ q)) (¬ (∧ p q)))
(→ (¬ p) (→ (¬ q) (¬ (∨ p q))))
(→ (∧ (¬ p) (¬ q)) (¬ (∨ p q)))
(↔ (∧ (¬ p) (¬ q)) (¬ (∨ p q)))
(→ (∧ p q) (¬ (∨ (¬ p) (¬ q))))
(→ (∨ p q) (¬ (∧ (¬ p) (¬ q))))
(∧ p q)(¬ (∨ (¬ p) (¬ q)))
(∨ p q)(¬ (∧ (¬ p) (¬ q)))
(∨ (¬ p) (¬ q))(¬ (∧ p q))
(∧ (¬ p) (¬ q))(¬ (∨ p q))
(¬ (∨ p q))(∧ (¬ p) (¬ q))
(→ (¬ (¬ (∧ p q))) (∧ (¬ (¬ p)) (¬ (¬ q))))
(→ (∨ (¬ (¬ p)) (¬ (¬ q))) (¬ (¬ (∨ p q))))
(→ p (→ q r))(→ (¬ (¬ p)) (→ (¬ (¬ q)) (¬ (¬ r))))
(→ (∧ (¬ (¬ p)) (¬ (¬ q))) (¬ (¬ (∧ p q))))
(↔ (∧ (¬ (¬ p)) (¬ (¬ q))) (¬ (¬ (∧ p q))))
(¬ (∧ p (¬ p)))
(→ (∧ (∨ p q) (∨ (¬ p) q)) q)
(→ (↔ p q) (↔ (¬ p) (¬ q)))
(↔ p q)(↔ (¬ p) (¬ q))
(→ (∧ (↔ p q) (↔ r s)) (→ (→ p r) (→ q r)))
(→ (∧ (↔ p q) (↔ r s)) (→ (→ q r) (→ q s)))
(→ (∧ (↔ p q) (↔ r s)) (→ (→ p r) (→ q s)))
(→ (∧ (↔ p q) (↔ r s)) (↔ (→ p r) (→ q s)))
(↔ p q) , (↔ r s)(↔ (→ p r) (→ q s))
(→ (∧ (↔ p q) (↔ r s)) (↔ (↔ p r) (↔ q s)))
(↔ p q) , (↔ r s)(↔ (↔ p r) (↔ q s))
(↔ (→ p (↔ q r)) (↔ (→ p q) (→ p r)))
(→ p (↔ q r))(↔ (→ p q) (→ p r))
(→ (∧ p (¬ q)) (¬ (→ p q)))
(→ (∨ p q) (→ (¬ p) q))
(∨ p q)(→ (¬ p) q)
(→ (∨ (¬ p) q) (→ p q))
(∨ (¬ p) q)(→ p q)
(→ (¬ (→ p q)) (¬ (∨ (¬ p) q)))
(→ (¬ (→ (¬ p) q)) (¬ (∨ p q)))
(→ (¬ (∨ p q)) (¬ (→ (¬ p) q)))
(↔ (¬ (∨ p q)) (¬ (→ (¬ p) q)))
(→ (∧ (∨ (¬ p) q) (∨ p (¬ q))) (↔ p q))
(∧ (∨ (¬ p) q) (∨ p (¬ q)))(↔ p q)
(∨ (¬ p) q) , (∨ p (¬ q))(↔ p q)
(→ (∧ p q) (→ p q))
(→ (∧ p q) (↔ p q))
(↔ (⊤) (¬ (∧ p (¬ p))))
(↔ (→ p p) (⊤))
(↔ (⊥) (¬ (⊤)))
(¬ (⊥))
(→ (∧ p (¬ p)) (⊥))
(→ (⊥) (∧ p (¬ p)))
(↔ (∧ p (¬ p)) (⊥))
(→ (¬ p) (→ p (⊥)))
(→ (→ p (⊥)) (¬ p))
(↔ (¬ p) (→ p (⊥)))
(¬ p)(→ p (⊥))
(→ p (⊥))(¬ p)