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 1531) and the constant false ⊥ (df-fal 1541), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1573), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1574), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1575), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1576). Contrast with ∧ (df-an 397), ∨ (df-or 842), → (wi 4), and ⊼ (df-nan 1476). (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 1495 | . 2 wff (𝜑 ⊻ 𝜓) |
4 | 1, 2 | wb 207 | . . 3 wff (𝜑 ↔ 𝜓) |
5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ↔ 𝜓) |
6 | 3, 5 | wb 207 | 1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: xnor 1497 xorcom 1498 xorass 1499 excxor 1500 xor2 1501 xorneg2 1505 xorbi12i 1508 xorbi12d 1509 anxordi 1510 xorexmid 1511 truxortru 1573 truxorfal 1574 falxorfal 1576 hadbi 1589 elsymdifxor 4225 sadadd2lem2 15789 f1omvdco3 18508 bj-bixor 33823 tsxo3 35300 tsxo4 35301 ifpxorxorb 39757 or3or 40251 axorbtnotaiffb 43020 axorbciffatcxorb 43022 aisbnaxb 43028 abnotbtaxb 43032 abnotataxb 43033 afv2orxorb 43308 |
Copyright terms: Public domain | W3C validator |