Theorem pm2.21fal

Description: If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.21fal.1	$$⊢\phi \to \psi$$
2		pm2.21fal.2	$$⊢\phi \to \neg \psi$$
3	1 2	pm2.21dd	$$⊢\phi \to \perp$$