Theorem pm2.21dd

Description: A contradiction implies anything. Deduction from pm2.21 . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof shortened by Wolf Lammen, 22-Jul-2019)

	Ref	Expression
Hypotheses	pm2.21dd.1	$$⊢\phi \to \psi$$
	pm2.21dd.2	$$⊢\phi \to \neg \psi$$
Assertion	pm2.21dd	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.21dd.1	$$⊢\phi \to \psi$$
2		pm2.21dd.2	$$⊢\phi \to \neg \psi$$
3	1 2	pm2.65i	$$⊢\neg \phi$$
4	3	pm2.21i	$$⊢\phi \to \chi$$