![]() |
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 104), ∨ (wo 708), 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 1375 | . 2 wff (𝜑 ⊻ 𝜓) |
4 | 1, 2 | wo 708 | . . 3 wff (𝜑 ∨ 𝜓) |
5 | 1, 2 | wa 104 | . . . 4 wff (𝜑 ∧ 𝜓) |
6 | 5 | wn 3 | . . 3 wff ¬ (𝜑 ∧ 𝜓) |
7 | 4, 6 | wa 104 | . 2 wff ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) |
8 | 3, 7 | wb 105 | 1 wff ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) |
Colors of variables: wff set class |
This definition is referenced by: xoranor 1377 xorbi2d 1380 xorbi1d 1381 xorbin 1384 xorcom 1388 xornbidc 1391 xordc1 1393 anxordi 1400 truxortru 1419 truxorfal 1420 falxortru 1421 falxorfal 1422 mptxor 1424 reapltxor 8533 zeoxor 11854 odd2np1 11858 bdxor 14241 trirec0xor 14446 |
Copyright terms: Public domain | W3C validator |