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 698), 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 1364 | . 2 wff (𝜑 ⊻ 𝜓) |
4 | 1, 2 | wo 698 | . . 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 1366 xorbi2d 1369 xorbi1d 1370 xorbin 1373 xorcom 1377 xornbidc 1380 xordc1 1382 anxordi 1389 truxortru 1408 truxorfal 1409 falxortru 1410 falxorfal 1411 mptxor 1413 reapltxor 8478 zeoxor 11791 odd2np1 11795 bdxor 13559 trirec0xor 13765 |
Copyright terms: Public domain | W3C validator |