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 385 | . . 3 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓)) | |
2 | 1 | con2bii 360 | . 2 ⊢ ((𝜑 ↔ ¬ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
3 | 2 | bicomi 226 | 1 ⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 |
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 209 |
This theorem is referenced by: nbbn 387 pm5.15 1009 nbi2 1012 xorass 1504 hadnot 1599 nabbi 3121 notzfausOLD 5255 nmogtmnf 28541 nmopgtmnf 29639 limsucncmpi 33788 aiffnbandciffatnotciffb 43134 axorbciffatcxorb 43135 abnotbtaxb 43145 afv2orxorb 43421 line2ylem 44732 line2xlem 44734 |
Copyright terms: Public domain | W3C validator |