Metamath Proof Explorer


Theorem conimpf

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

Ref Expression
Hypotheses conimpf.1 𝜑
conimpf.2 ¬ 𝜓
conimpf.3 ( 𝜑𝜓 )
Assertion conimpf ( 𝜑 ↔ ⊥ )

Proof

Step Hyp Ref Expression
1 conimpf.1 𝜑
2 conimpf.2 ¬ 𝜓
3 conimpf.3 ( 𝜑𝜓 )
4 3 2 aibnbaif ( 𝜑 ↔ ⊥ )