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 102), (wo 661), 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 1306 | . 2 |
4 | 1, 2 | wo 661 | . . 3 |
5 | 1, 2 | wa 102 | . . . 4 |
6 | 5 | wn 3 | . . 3 |
7 | 4, 6 | wa 102 | . 2 |
8 | 3, 7 | wb 103 | 1 |
Colors of variables: wff set class |
This definition is referenced by: xoranor 1308 xorbi2d 1311 xorbi1d 1312 xorbin 1315 xorcom 1319 xornbidc 1322 xordc1 1324 anxordi 1331 truxortru 1350 truxorfal 1351 falxortru 1352 falxorfal 1353 mptxor 1355 reapltxor 7689 zeoxor 10268 odd2np1 10272 bdxor 10627 |
Copyright terms: Public domain | W3C validator |