Metamath Proof Explorer

Axiom ax-2

Description: AxiomFrege. Axiom A2 of Margaris p. 49. One of the 3 axioms of propositional calculus. It "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known asFrege in the literature; see Proposition 2 of Frege1879 p. 26. It is also proved as Theorem *2.77 of WhiteheadRussell p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 . (Contributed by NM, 30-Sep-1992)

Ref Expression
Assertion ax-2 φ ψ χ φ ψ φ χ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 wch wff χ
3 1 2 wi wff ψ χ
4 0 3 wi wff φ ψ χ
5 0 1 wi wff φ ψ
6 0 2 wi wff φ χ
7 5 6 wi wff φ ψ φ χ
8 4 7 wi wff φ ψ χ φ ψ φ χ