![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-xor | Unicode 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 1398) and the constant false (df-fal 1401), we will be
able to prove these truth table values:
(truxortru 1441), (truxorfal 1442),
(falxortru 1443), and
(falxorfal 1444). Contrast with /\
(df-an 371), \/ (df-or 370), -> (wi 4), and
-/\
(df-nan 1344) . (Contributed by FL,
22-Nov-2010.) |
Ref | Expression |
---|---|
df-xor |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | wps | . . 3 | |
3 | 1, 2 | wxo 1363 | . 2 |
4 | 1, 2 | wb 184 | . . 3 |
5 | 4 | wn 3 | . 2 |
6 | 3, 5 | wb 184 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: xnor 1365 xorcom 1366 xorass 1367 excxor 1368 xor2 1369 xorneg1 1373 xorbi12i 1376 xorbi12d 1377 anxordi 1378 xorexmid 1379 truxortru 1441 truxorfal 1442 falxortru 1443 falxorfal 1444 hadbi 1454 had0 1471 sadadd2lem2 14100 f1omvdco3 16474 tsxo3 30546 tsxo4 30547 axorbtnotaiffb 32098 axorbciffatcxorb 32100 aisbnaxb 32106 abnotbtaxb 32111 abnotataxb 32112 bj-ifxorxorb 37733 |
Copyright terms: Public domain | W3C validator |