![]() |
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 386 | . . 3 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓)) | |
2 | 1 | con2bii 361 | . 2 ⊢ ((𝜑 ↔ ¬ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
3 | 2 | bicomi 227 | 1 ⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 |
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 210 |
This theorem is referenced by: nbbn 388 pm5.15 1010 nbi2 1013 xorass 1507 hadnot 1604 nabbi 3089 notzfausOLD 5228 nmogtmnf 28553 nmopgtmnf 29651 limsucncmpi 33906 wl-3xorbi 34890 wl-3xornot 34898 aiffnbandciffatnotciffb 43497 axorbciffatcxorb 43498 abnotbtaxb 43508 afv2orxorb 43784 line2ylem 45165 line2xlem 45167 |
Copyright terms: Public domain | W3C validator |