Theorem orel2

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of WhiteheadRussell p. 107. (Contributed by NM, 12-Aug-1994) (Proof shortened by Wolf Lammen, 5-Apr-2013)

	Ref	Expression
Assertion	orel2	$$⊢\neg \phi \to \left(\left(\psi \vee \phi \right)\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		idd	$$⊢\neg \phi \to \left(\psi \to \psi \right)$$
2		pm2.21	$$⊢\neg \phi \to \left(\phi \to \psi \right)$$
3	1 2	jaod	$$⊢\neg \phi \to \left(\left(\psi \vee \phi \right)\to \psi \right)$$