Axiom ax-io 629

Description: Definition of 'or'. Axiom 6 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)

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 628	. . 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 97	. 2 wff ((φ → ψ) ∧ (χ → ψ))
9	5, 8	wb 98	1 wff (((φ ∨ χ) → ψ) ↔ ((φ → ψ) ∧ (χ → ψ)))

This axiom is referenced by:  jaob  630  bj-inf2vnlem1  9430