Axiom ax-io 710

Description: Definition of 'or'. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias jaob 711 instead. (New usage is discouraged.)

Assertion

Ref	Expression
ax-io	|- ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )

Detailed syntax breakdown of Axiom ax-io

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff ph
2		wch	. . . 4 wff ch
3	1, 2	wo 709	. . 3 wff ( ph \/ ch )
4		wps	. . 3 wff ps
5	3, 4	wi 4	. 2 wff ( ( ph \/ ch ) -> ps )
6	1, 4	wi 4	. . 3 wff ( ph -> ps )
7	2, 4	wi 4	. . 3 wff ( ch -> ps )
8	6, 7	wa 104	. 2 wff ( ( ph -> ps ) /\ ( ch -> ps ) )
9	5, 8	wb 105	1 wff ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )

This axiom is referenced by:  jaob  711