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	⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)))

Detailed syntax breakdown of Axiom ax-io

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		wch	. . . 4 wff 𝜒
3	1, 2	wo 709	. . 3 wff (𝜑 ∨ 𝜒)
4		wps	. . 3 wff 𝜓
5	3, 4	wi 4	. 2 wff ((𝜑 ∨ 𝜒) → 𝜓)
6	1, 4	wi 4	. . 3 wff (𝜑 → 𝜓)
7	2, 4	wi 4	. . 3 wff (𝜒 → 𝜓)
8	6, 7	wa 104	. 2 wff ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))
9	5, 8	wb 105	1 wff (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)))

This axiom is referenced by:  jaob  711