Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-xor | GIF 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 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 1, 2 | wxo 1353 | . 2 wff (𝜑 ⊻ 𝜓) |
4 | 1, 2 | wo 697 | . . 3 wff (𝜑 ∨ 𝜓) |
5 | 1, 2 | wa 103 | . . . 4 wff (𝜑 ∧ 𝜓) |
6 | 5 | wn 3 | . . 3 wff ¬ (𝜑 ∧ 𝜓) |
7 | 4, 6 | wa 103 | . 2 wff ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) |
8 | 3, 7 | wb 104 | 1 wff ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
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 8351 zeoxor 11566 odd2np1 11570 bdxor 13034 |
Copyright terms: Public domain | W3C validator |