Metamath Proof Explorer
Description: If a wff and its negation are provable, then falsum is provable.
(Contributed by Mario Carneiro, 9Feb2017)


Ref 
Expression 

Hypotheses 
pm2.21fal.1 
$${\u22a2}{\phi}\to {\psi}$$ 


pm2.21fal.2 
$${\u22a2}{\phi}\to \neg {\psi}$$ 

Assertion 
pm2.21fal 
$${\u22a2}{\phi}\to \perp $$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

pm2.21fal.1 
$${\u22a2}{\phi}\to {\psi}$$ 
2 

pm2.21fal.2 
$${\u22a2}{\phi}\to \neg {\psi}$$ 
3 
1 2

pm2.21dd 
$${\u22a2}{\phi}\to \perp $$ 