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 | ⊢ ( 𝜑 ↔ ⊥ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | conimpf.1 | ⊢ 𝜑 | |
2 | conimpf.2 | ⊢ ¬ 𝜓 | |
3 | conimpf.3 | ⊢ ( 𝜑 → 𝜓 ) | |
4 | 3 2 | aibnbaif | ⊢ ( 𝜑 ↔ ⊥ ) |