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 (wa 103), (wo 697), and (wi 4) . (Contributed by FL, 22-Nov-2010.) (Modified by Jim Kingdon, 1-Mar-2018.) |
Ref | Expression |
---|---|
df-xor |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | wps | . . 3 | |
3 | 1, 2 | wxo 1353 | . 2 |
4 | 1, 2 | wo 697 | . . 3 |
5 | 1, 2 | wa 103 | . . . 4 |
6 | 5 | wn 3 | . . 3 |
7 | 4, 6 | wa 103 | . 2 |
8 | 3, 7 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: xoranor 1355 xorbi2d 1358 xorbi1d 1359 xorbin 1362 xorcom 1366 xornbidc 1369 xordc1 1371 anxordi 1378 truxortru 1397 truxorfal 1398 falxortru 1399 falxorfal 1400 mptxor 1402 reapltxor 8344 zeoxor 11555 odd2np1 11559 bdxor 13023 |
Copyright terms: Public domain | W3C validator |