![]() |
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 1536) and the constant false ⊥ (df-fal 1546), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1578), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1579), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1580), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1581). Contrast with ∧ (df-an 396), ∨ (df-or 845), → (wi 4), and ⊼ (df-nan 1485). (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 1504 | . 2 wff (𝜑 ⊻ 𝜓) |
4 | 1, 2 | wb 205 | . . 3 wff (𝜑 ↔ 𝜓) |
5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ↔ 𝜓) |
6 | 3, 5 | wb 205 | 1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: xnor 1506 xorcom 1507 xorass 1508 excxor 1509 xor2 1510 xorneg2 1514 xorbi12i 1517 xorbi12d 1518 anxordi 1519 xorexmid 1520 truxortru 1578 truxorfal 1579 falxorfal 1581 hadbi 1591 elsymdifxor 4242 sadadd2lem2 16390 f1omvdco3 19361 bj-bixor 35960 wl-df3xor2 36841 wl-3xorbi 36845 wl-2xor 36855 tsxo3 37501 tsxo4 37502 oneptri 42520 ifpxorxorb 42776 or3or 43288 axorbtnotaiffb 46123 axorbciffatcxorb 46125 aisbnaxb 46131 abnotbtaxb 46135 abnotataxb 46136 afv2orxorb 46446 |
Copyright terms: Public domain | W3C validator |