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	$$⊢\left(\left(\phi \vee \chi \right)\to \psi \right)\leftrightarrow \left(\left(\phi \to \psi \right)\wedge \left(\chi \to \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		jaob	$$⊢\left(\left(\phi \vee \chi \right)\to \psi \right)\leftrightarrow \left(\left(\phi \to \psi \right)\wedge \left(\chi \to \psi \right)\right)$$