This page details some theorems to be used later. For each theorem, either I would note that it is a theorem of the formal system used on Metamath.org, or I would provide a proof of it.

Note: Metamath.org is a continually updated site, thus the current numbering of their theorems here may be outdated.

Abbreviation key

• 'th.#' : 'Theorem #'

• 'MM' : 'metamath.org'

• 'H' : 'Hypothesis'

• 'QED' : 'End of proof'

• 'MP' : 'modus ponens', 'ax.4'

• 'MT' : 'modus tollens', 'th.13'

• 'HS' : 'Hypothetical syllogism', 'th.5'

• '&-intro' : 'Conjunction introduction', 'th.9'

• '&-elim' : 'Conjunction elimination', 'th.21'

• '∨-intro' : 'Disjunction introduction', 'th.16'

• '∀-gen.' : 'Generalization', 'ax.5'

• '∃-gen.' : 'Existential generalization', 'th.52'

• '∀I' : 'Universal instantiation', 'th.65'

Theorems utilizing only Axioms 1 - 6

1. Th. 1: ⊢ A → A 'Identity' (Theorem 22 of Metamath)

2. Th. 2: ⊢(A ≝ B) , ⊢(A → A) ⇒ ⊢(A → B)

   1. Proof:

      1. A ≝ B (hypothesis 1)

      2. A → A (hypothesis 2)

      3. A → B (1, 2 Ax. 5) QED

3. ⊢(A ≝ B) ⇒ ⊢(A → B)

   1. Proof:

      1. A ≝ B (hypothesis)

      2. A → A (th.1)

      3. A → B (1, 2, th.2) QED

4. ⊢(A ≝ B) ⇒ ⊢(B → A)

   2. 1. A ≝ B (H)

      2. A → A (th.1)

      3. B → A (1, 2, Ax. 5) QED

5. ⊢(A → B) , ⊢(B → C) ⇒ ⊢(A → C) 'Hypothetical syllogism' (Th. 17 of MM)

6. ⊢[¬(A → ¬B) → C] ⇒ ⊢[A → (B → C)] (Th. 155 of MM)

7. ⊢[(A & B) → C] ⇒ ⊢[A → (B → C)]

   1. (A & B) → C (hypothesis)

   2. (A & B) ≝ ¬(A → ¬B) (def. of &)

   3. ¬(A → ¬B) → (A & B) (2, th.4 [¬(A → ¬B) / B | (A & B) / A ] )

   4. ¬(A → ¬B) → C (3, 1, th.5)

   5. A → (B → C) (4, th.6) QED

8. ⊢ A → [B → (A & B)]

   1. (A & B) → (A & B) (Identity)

   2. A → [B → (A & B)] (1, th.7 [(A & B) / C] ) QED

9. ⊢A , ⊢B ⇒ ⊢(A & B) 'Conjunction introduction'

   1. A (H1)

   2. B (H2)

   3. A → [B → (A & B)] (th.8)

   4. B → (A & B) (1, 3, ax.4 'MP')

   5. A & B (2, 4, MP) QED

10. ⊢(A ≝ B) ⇒ ⊢(A ↔︎ B) (Remarks: This theorem is significant because it allows me to use the proofs on Metamath that involve defined symbols. I wasn't able to do so before this because Metamath uses ↔︎ for defining new symbols while I use ≝ for doing so.)

    1. A ≝ B (H)

    2. A → B (1, th. 3)

    3. B → A (1, th. 4)

    4. (A → B) & (B → A) (2, 3, th.9)

    5. (A ↔︎ B) ≝ [(A → B) & (B → A)] (def. of ↔︎)

    6. [(A → B) & (B → A)] → (A ↔︎ B) (5, th. 4)

    7. A ↔︎ B (4, 6 MP) QED

11. ⊢ ¬¬A ↔︎ A 'Double negation intr./elim.' (Th. 298 of MM)

12. ⊢ (¬A → A) → A 'Clavius's law' (Th. 114 of MM)

13. ⊢(A → B) , ⊢¬B ⇒ ⊢¬A 'Modus tollens' (Th. 182 of MM)

14. ⊢ (A → ¬A) → ¬A 'a self-refuting hypothesis is false' (Th. 174 of MM)

15. ⊢(A → B) , ⊢(A → ¬ B) ⇒ ⊢¬A 'Reductio ad absurdum' (Th. 179 of MM)

16. ⊢A ⇒ ⊢(A ∨ B) 'Disjunction introduction' (Th. 399 of MM)

17. ⊢ A ∨ ¬A 'Law of excluded middle' (Th. 423 of MM)

18. ⊢ (A → B) ↔︎ (¬A ∨ B) 'Conditional exchange' (Th. 420 of MM)

19. ⊢ [(A & B) → C] ↔︎ [A → (B → C)] 'Importation-exportation' (Th. 454 of MM)

20. ⊢ (A → B) ↔︎ ¬(A & ¬B) (Th. 432 of MM)

21. ⊢(A & B) ⇒ ⊢A 'Conjunction elimination' (Th. 466 of MM)

22. ⊢ ¬(A & B) ↔︎ (¬A ∨ ¬B) 'De Morgan's law 1' (Th. 501 of MM)

23. ⊢ ¬(A ∨ B) ↔︎ (¬A & ¬B) 'De Morgan's law 2' (Th. 503 of MM)

24. ⊢ A ↔︎ (A ∨ A) 'Idempotence of disjunction' (Th. 528 of MM)

25. ⊢ A ↔︎ (A & A) 'Idempotence of conjunction' (Th. 664 of MM)

26. ⊢ (A ∨ B) ↔︎ (B ∨ A) 'Commutativity of disjunction' (Th. 395 of MM)

27. ⊢ (A & B) ↔︎ (B & A) 'Commutativity of conjunction' (Th. 458 of MM)

28. ⊢ (A ↔︎ B) ↔︎ (B ↔︎ A) 'Commutativity of biconditional' (Th. 205 of MM)

29. ⊢ ¬(A & ¬A) 'Law of non-contradiction' (Th. 909 of MM)

30. ⊢ [(A ∨ B) ∨ C] ↔︎ [A ∨ (B ∨ C)] 'Associativity of disjunction' (Th. 538 of MM)

31. [(A & B) & C] ↔︎ [A & (B & C)] 'Associativity of conjunction' (Th. 669 of MM)

32. ⊢(A ∨ B) , ⊢¬B ⇒ ⊢A 'Disjunctive syllogism' (Th. 1679 of MM)

33. ⊢(A ⊻ B) ↔︎ [(A ∨ B) & ¬(A & B)] 'Exclusive disjunction' (Th. 1450 of MM)

34. ⊢(A ⊻ B) ↔︎ (B ⊻ A) 'Commutativity of exclusive disjunction' (Th. 1446 of MM)

35. [(A ⊻ B) ⊻ C] ↔︎ [A ⊻ (B ⊻ C)] 'Associativity of exclusive disjunction' (Th. 1447 of MM)

36. ⊢(A ⊻ B) , ⊢¬B ⇒ ⊢A 'Exclusive disjunction elimination' (Th. 1680 of MM)

37. ⊢ (A & ¬ A) → B 'Explosion' (a contradiction / false SoA implies anything) (similar to Th. 112 and Th. 1479 of MM)

    1. ¬(A & ¬A) (th.29)

    2. ¬(A & ¬A) ∨ B (1, th.16)

    3. (A & ¬A) → B (2, Th. 422 of MM) QED

Theorems utilizing only Axioms 1 - 13

38. ⊢ (∀x)¬Px ↔︎ ¬(∃x)Px 'if everything isn't P then nothing is P, and vice versa' (Th. 1691 of MM)

39. ⊢ (∀x)Px ↔︎ ¬(∃x)¬Px 'if everything is P then there isn't anything that isn't P, and vice versa' (Th. 1726 of MM)

40. ⊢ (∃x)¬Px ↔︎ ¬(∀x)Px 'if there is something that isn't P, then not everything is P, and vice versa' (Th. 1727 of MM)

41. ⊢ (∃x)(Px & Qx) → [(∃x)Px & (∃x)Qx] 'Existentially quantified conjunction' (Th. 1759 of MM)

42. ⊢ (∀x)(Px & Qx) ↔︎ [(∀x)Px & (∀x)Qx] 'Universally quantified conjunction' (Th. 1760 of MM)

43. ⊢ (∃x)(Px ∨ Qx) ↔︎ [(∃x)Px ∨ (∃x)Qx] 'Existentially quantified disjunction' (note the difference from th.41) (Th. 1773 of MM)

44. ⊢ [(∀x)Px ∨ (∀x)Qx] → (∀x)(Px ∨ Qx) 'Universally quantified disjunction' (note the difference from th.42) (Th. 1775 of MM)

45. ⊢(∀x)(Px → Qx) , ⊢Pa ⇒ ⊢Qa 'Universal modus ponens' (Th. 1697 of MM)

46. ⊢(Aa → Ba) ⇒ ⊢[(∃x)A[x/a] → (∃x)B[x/a]] (Th. 1735 of MM)

47. ⊢(∃x)Px , ⊢(Pa → Qa) ⇒ ⊢(∃x)Qx 'Existential modus ponens' (Th. 1737 of MM)

48. ⊢ [(∀x)(Ax → Bx) & (∀x)(Bx → Cx)] → (∀x)(Ax → Cx) 'Universal hypothetical implication' (related to Aristotle's 'Barbara' syllogism) (Th. 1785 of MM)

49. ⊢[A(b, c, ...) → B(a)] ⇒ ⊢(A(b, c, ...) → (∀x)B[x/a]) provided that 'a' doesn't occur in the wff 'A'

'Universal generalization' (Th. 1801 of MM) (one of the rules of inference of Natural Deduction that lets one generalizes from an arbitrary individual object)

1. A(b, c, ...) → B(a) (H)

2. A(b, c, ...) → (∀[x/a])A provided that 'a' doesn't occur in the wff 'A' (Ax. 9)

3. (∀x)A → (∀x)B(x) (1, Th. 1710 of MM)

4. A(b, c, ...) → (∀x)B(x) (2, 3, HS) QED