Description: A contraposition inference. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 13-Oct-2012)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | con1bii.1 | ⊢ ( ¬ 𝜑 ↔ 𝜓 ) | |
| Assertion | con1bii | ⊢ ( ¬ 𝜓 ↔ 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con1bii.1 | ⊢ ( ¬ 𝜑 ↔ 𝜓 ) | |
| 2 | notnotb | ⊢ ( 𝜑 ↔ ¬ ¬ 𝜑 ) | |
| 3 | 2 1 | xchbinx | ⊢ ( 𝜑 ↔ ¬ 𝜓 ) |
| 4 | 3 | bicomi | ⊢ ( ¬ 𝜓 ↔ 𝜑 ) |