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 428.

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 10  id1 16  a2d 19  pm2.04OLD 73  dfbi1gb 239  imdi 427  pm5.41OLD 429  sbi1 1907  ralim 2444  difin0ss 3172  bnj1102 13848  bnj1126 13861

Copyright terms: Public domain