Theorem axio

Description: Definition of 'or' (intuitionistic logic axiom ax-io). (Contributed by Jim Kingdon, 21-May-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	axio	⊢ ( ( ( 𝜑 ∨ 𝜒 ) → 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		jaob	⊢ ( ( ( 𝜑 ∨ 𝜒 ) → 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜓 ) ) )