![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-xor | Structured version Visualization version GIF version |
Description: Define exclusive disjunction (logical "xor"). Return true if either the left or right, but not both, are true. After we define the constant true ⊤ (df-tru 1662) and the constant false ⊥ (df-fal 1672), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1704), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1705), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1706), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1707). Contrast with ∧ (df-an 387), ∨ (df-or 881), → (wi 4), and ⊼ (df-nan 1615). (Contributed by FL, 22-Nov-2010.) |
Ref | Expression |
---|---|
df-xor | ⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 1, 2 | wxo 1639 | . 2 wff (𝜑 ⊻ 𝜓) |
4 | 1, 2 | wb 198 | . . 3 wff (𝜑 ↔ 𝜓) |
5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ↔ 𝜓) |
6 | 3, 5 | wb 198 | 1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: xnor 1641 xorcom 1642 xorass 1643 excxor 1644 xor2 1645 xorneg2 1649 xorbi12i 1652 xorbi12d 1653 anxordi 1654 xorexmid 1655 truxortru 1704 truxorfal 1705 falxorfal 1707 hadbi 1713 elsymdifxor 4078 sadadd2lem2 15546 f1omvdco3 18220 tsxo3 34487 tsxo4 34488 ifpxorxorb 38699 or3or 39160 axorbtnotaiffb 41865 axorbciffatcxorb 41867 aisbnaxb 41873 abnotbtaxb 41877 abnotataxb 41878 afv2orxorb 42131 |
Copyright terms: Public domain | W3C validator |