Axiom ax-2 5

Description: Axiom Frege. 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 as Frege in the literature. 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 169.

Assertion

Ref	Expression
ax-2	⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))

Detailed syntax breakdown of Axiom ax-2

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . . 4 wff ψ
3		wch	. . . 4 wff χ
4	2, 3	wi 3	. . 3 wff (ψ → χ)
5	1, 4	wi 3	. 2 wff (φ → (ψ → χ))
6	1, 2	wi 3	. . 3 wff (φ → ψ)
7	1, 3	wi 3	. . 3 wff (φ → χ)
8	6, 7	wi 3	. 2 wff ((φ → ψ) → (φ → χ))
9	5, 8	wi 3	1 wff ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))

This axiom is referenced by:  a2i 9  a2d 13  pm2.04 30  id1 60  biigb 159  imdi 168  pm5.41 169  sbi1 1230  r19.20 1699  difin0ss 2328

Copyright terms: Public domain