Description: A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993) (Proof shortened by Wolf Lammen, 12-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mt2bi.1 | ⊢ 𝜑 | |
| Assertion | mt2bi | ⊢ ( ¬ 𝜓 ↔ ( 𝜓 → ¬ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mt2bi.1 | ⊢ 𝜑 | |
| 2 | 1 | a1bi | ⊢ ( ¬ 𝜓 ↔ ( 𝜑 → ¬ 𝜓 ) ) |
| 3 | con2b | ⊢ ( ( 𝜑 → ¬ 𝜓 ) ↔ ( 𝜓 → ¬ 𝜑 ) ) | |
| 4 | 2 3 | bitri | ⊢ ( ¬ 𝜓 ↔ ( 𝜓 → ¬ 𝜑 ) ) |