Metamath Proof Explorer
Description: Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1Sep2016)


Ref 
Expression 

Hypotheses 
aibnbaif.1 
$${\u22a2}{\phi}\to {\psi}$$ 


aibnbaif.2 
$${\u22a2}\neg {\psi}$$ 

Assertion 
aibnbaif 
$${\u22a2}{\phi}\leftrightarrow \perp $$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

aibnbaif.1 
$${\u22a2}{\phi}\to {\psi}$$ 
2 

aibnbaif.2 
$${\u22a2}\neg {\psi}$$ 
3 
1 2

aibnbna 
$${\u22a2}\neg {\phi}$$ 
4 
3

bifal 
$${\u22a2}{\phi}\leftrightarrow \perp $$ 