| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE 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. Contrast with |
| Ref | Expression |
|---|---|
| df-xor |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . 3
| |
| 2 | wps |
. . 3
| |
| 3 | 1, 2 | wxo 1394 |
. 2
|
| 4 | 1, 2 | wo 709 |
. . 3
|
| 5 | 1, 2 | wa 104 |
. . . 4
|
| 6 | 5 | wn 3 |
. . 3
|
| 7 | 4, 6 | wa 104 |
. 2
|
| 8 | 3, 7 | wb 105 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: xoranor 1396 xorbi2d 1399 xorbi1d 1400 xorbin 1403 xorcom 1407 xornbidc 1410 xordc1 1412 anxordi 1419 truxortru 1438 truxorfal 1439 falxortru 1440 falxorfal 1441 mptxor 1443 reapltxor 8661 zeoxor 12122 odd2np1 12126 bdxor 15705 trirec0xor 15917 |
| Copyright terms: Public domain | W3C validator |