Axiom ax-2 4

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.

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 2	. . 3 wff (ps -> ch)
5	1, 4	wi 2	. 2 wff (ph -> (ps -> ch))
6	1, 2	wi 2	. . 3 wff (ph -> ps)
7	1, 3	wi 2	. . 3 wff (ph -> ch)
8	6, 7	wi 2	. 2 wff ((ph -> ps) -> (ph -> ch))
9	5, 8	wi 2	1 wff ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))

This axiom is referenced by:  a2i 8  id1 10  a2d 15  pm2.04 31  biigb 129  imdi 147  sbi1 884  r19.20 1251  difin0ss 1753

metamath.org