Description: Theorem *5.18 of WhiteheadRussell p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002) (Proof shortened by Andrew Salmon, 20-Jun-2011) (Proof shortened by Wolf Lammen, 15-Oct-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pm5.18 | ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ↔ ¬ 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm5.501 | ⊢ ( 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑 ↔ ¬ 𝜓 ) ) ) | |
| 2 | 1 | con1bid | ⊢ ( 𝜑 → ( ¬ ( 𝜑 ↔ ¬ 𝜓 ) ↔ 𝜓 ) ) |
| 3 | pm5.501 | ⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) ) | |
| 4 | 2 3 | bitr2d | ⊢ ( 𝜑 → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ↔ ¬ 𝜓 ) ) ) |
| 5 | nbn2 | ⊢ ( ¬ 𝜑 → ( ¬ ¬ 𝜓 ↔ ( 𝜑 ↔ ¬ 𝜓 ) ) ) | |
| 6 | 5 | con1bid | ⊢ ( ¬ 𝜑 → ( ¬ ( 𝜑 ↔ ¬ 𝜓 ) ↔ ¬ 𝜓 ) ) |
| 7 | nbn2 | ⊢ ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) ) | |
| 8 | 6 7 | bitr2d | ⊢ ( ¬ 𝜑 → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ↔ ¬ 𝜓 ) ) ) |
| 9 | 4 8 | pm2.61i | ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ↔ ¬ 𝜓 ) ) |