Theorem rb-ax3

Description: The third of four axioms in the Russell-Bernays axiom system. (Contributed by Anthony Hart, 13-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	rb-ax3	$$⊢\left(\neg \phi \vee \left(\psi \vee \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm2.46	$$⊢\neg \left(\psi \vee \phi \right)\to \neg \phi$$
2	1	con1i	$$⊢\neg \neg \phi \to \left(\psi \vee \phi \right)$$
3	2	orri	$$⊢\left(\neg \phi \vee \left(\psi \vee \phi \right)\right)$$