Description: Two ways to express exclusive disjunction ( df-xor ). Theorem *5.22 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 22-Jan-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xor | ⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iman | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ¬ ( 𝜑 ∧ ¬ 𝜓 ) ) | |
| 2 | iman | ⊢ ( ( 𝜓 → 𝜑 ) ↔ ¬ ( 𝜓 ∧ ¬ 𝜑 ) ) | |
| 3 | 1 2 | anbi12i | ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ↔ ( ¬ ( 𝜑 ∧ ¬ 𝜓 ) ∧ ¬ ( 𝜓 ∧ ¬ 𝜑 ) ) ) |
| 4 | dfbi2 | ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ) | |
| 5 | ioran | ⊢ ( ¬ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ¬ ( 𝜑 ∧ ¬ 𝜓 ) ∧ ¬ ( 𝜓 ∧ ¬ 𝜑 ) ) ) | |
| 6 | 3 4 5 | 3bitr4ri | ⊢ ( ¬ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( 𝜑 ↔ 𝜓 ) ) |
| 7 | 6 | con1bii | ⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) ) |