This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005)
(Proof shortened by Wolf Lammen, 24-Jan-2013)
|
|
Ref |
Expression |
|
Assertion |
nbi2 |
⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ¬ ( 𝜑 ∧ 𝜓 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
xor3 |
⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) ) |
| 2 |
|
pm5.17 |
⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∧ ¬ ( 𝜑 ∧ 𝜓 ) ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) ) |
| 3 |
1 2
|
bitr4i |
⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∧ ¬ ( 𝜑 ∧ 𝜓 ) ) ) |