Definition df-xor 1513

Description: Define exclusive disjunction (logical "xor"). Return true if either the left or right, but not both, are true. After we define the constant true ⊤ (df-tru 1544) and the constant false ⊥ (df-fal 1554), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1586), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1587), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1588), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1589). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1493). (Contributed by FL, 22-Nov-2010.)

Assertion

Ref	Expression
df-xor	⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wxo 1512	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 206	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1514  xorcom  1515  xorass  1516  excxor  1517  xor2  1518  xorneg2  1522  xorbi12i  1525  xorbi12d  1526  anxordi  1527  xorexmid  1528  truxortru  1586  truxorfal  1587  falxorfal  1589  hadbi  1599  elsymdifxor  4210  sadadd2lem2  16358  f1omvdco3  19359  bj-bixor  36624  wl-df3xor2  37502  wl-3xorbi  37506  wl-2xor  37516  tsxo3  38178  tsxo4  38179  oneptri  43289  ifpxorxorb  43543  or3or  44055  axorbtnotaiffb  46933  axorbciffatcxorb  46935  aisbnaxb  46941  abnotbtaxb  46945  abnotataxb  46946  afv2orxorb  47258