![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-xor | Structured version Visualization version 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
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-xor |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | wps |
. . 3
![]() ![]() | |
3 | 1, 2 | wxo 1415 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 2 | wb 189 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | wn 3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | wb 189 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: xnor 1417 xorcom 1418 xorass 1419 xorassOLD 1420 excxor 1421 xor2 1422 xorneg2 1426 xorneg1OLD 1428 xorbi12i 1431 xorbi12d 1432 anxordi 1433 xorexmid 1434 truxortru 1502 truxorfal 1503 falxortruOLD 1505 falxorfal 1506 hadbi 1512 sadadd2lem2 14479 f1omvdco3 17145 tsxo3 32427 tsxo4 32428 ifpxorxorb 36201 axorbtnotaiffb 38625 axorbciffatcxorb 38627 aisbnaxb 38633 abnotbtaxb 38638 abnotataxb 38639 |
Copyright terms: Public domain | W3C validator |