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	|- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))

Detailed syntax breakdown of Axiom ax-2

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . . 4 wff ps
3		wch	. . . 4 wff ch
4	2, 3	wi 3	. . 3 wff (ps -> ch)
5	1, 4	wi 3	. 2 wff (ph -> (ps -> ch))
6	1, 2	wi 3	. . 3 wff (ph -> ps)
7	1, 3	wi 3	. . 3 wff (ph -> ch)
8	6, 7	wi 3	. 2 wff ((ph -> ps) -> (ph -> ch))
9	5, 8	wi 3	1 wff ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))

This axiom is referenced by:  a2i 9  a2d 13  pm2.04 30  id1 60  dfbi1gb 159  imdi 168  pm5.41 169  sbi1 1234  r19.20 1705  difin0ss 2337

Copyright terms: Public domain