Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xor3 | Structured version Visualization version GIF version |
Description: Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006.) |
Ref | Expression |
---|---|
xor3 | ⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.18 383 | . . 3 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓)) | |
2 | 1 | con2bii 359 | . 2 ⊢ ((𝜑 ↔ ¬ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
3 | 2 | bicomi 225 | 1 ⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 |
This theorem is referenced by: nbbn 385 pm5.15 1006 nbi2 1009 xorass 1499 hadnot 1594 nabbi 3118 notzfausOLD 5254 nmogtmnf 28474 nmopgtmnf 29572 limsucncmpi 33690 aiffnbandciffatnotciffb 43017 axorbciffatcxorb 43018 abnotbtaxb 43028 afv2orxorb 43304 line2ylem 44666 line2xlem 44668 |
Copyright terms: Public domain | W3C validator |