|   | 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 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1584), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1585), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1586), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1587). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1491). (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 1510 | . 2 wff (𝜑 ⊻ 𝜓) | 
| 4 | 1, 2 | wb 206 | . . 3 wff (𝜑 ↔ 𝜓) | 
| 5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ↔ 𝜓) | 
| 6 | 3, 5 | wb 206 | 1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: xnor 1512 xorcom 1513 xorass 1514 excxor 1515 xor2 1516 xorneg2 1520 xorbi12i 1523 xorbi12d 1524 anxordi 1525 xorexmid 1526 truxortru 1584 truxorfal 1585 falxorfal 1587 hadbi 1597 elsymdifxor 4259 sadadd2lem2 16488 f1omvdco3 19468 bj-bixor 36593 wl-df3xor2 37471 wl-3xorbi 37475 wl-2xor 37485 tsxo3 38147 tsxo4 38148 oneptri 43274 ifpxorxorb 43529 or3or 44041 axorbtnotaiffb 46920 axorbciffatcxorb 46922 aisbnaxb 46928 abnotbtaxb 46932 abnotataxb 46933 afv2orxorb 47245 | 
| Copyright terms: Public domain | W3C validator |