Metamath Proof Explorer


Theorem conimpfalt

Description: Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016)

Ref Expression
Hypotheses conimpfalt.1 φ
conimpfalt.2 ¬ ψ
conimpfalt.3 φ ψ
Assertion conimpfalt φ

Proof

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