Metamath Proof Explorer

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	⊢ ( ¬ 𝜑 → ( ( 𝜓 ∨ 𝜑 ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		idd	⊢ ( ¬ 𝜑 → ( 𝜓 → 𝜓 ) )
2		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
3	1 2	jaod	⊢ ( ¬ 𝜑 → ( ( 𝜓 ∨ 𝜑 ) → 𝜓 ) )