Metamath Proof Explorer


Theorem aibnbaif

Description: Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016)

Ref Expression
Hypotheses aibnbaif.1 φ ψ
aibnbaif.2 ¬ ψ
Assertion aibnbaif φ

Proof

Step Hyp Ref Expression
1 aibnbaif.1 φ ψ
2 aibnbaif.2 ¬ ψ
3 1 2 aibnbna ¬ φ
4 3 bifal φ