Definition df-xor 1508

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 1539) and the constant false ⊥ (df-fal 1549), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1581), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1582), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1583), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1584). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1488). (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 1507	. 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  1509  xorcom  1510  xorass  1511  excxor  1512  xor2  1513  xorneg2  1517  xorbi12i  1520  xorbi12d  1521  anxordi  1522  xorexmid  1523  truxortru  1581  truxorfal  1582  falxorfal  1584  hadbi  1594  elsymdifxor  4265  sadadd2lem2  16483  f1omvdco3  19481  bj-bixor  36573  wl-df3xor2  37451  wl-3xorbi  37455  wl-2xor  37465  tsxo3  38125  tsxo4  38126  oneptri  43245  ifpxorxorb  43500  or3or  44012  axorbtnotaiffb  46852  axorbciffatcxorb  46854  aisbnaxb  46860  abnotbtaxb  46864  abnotataxb  46865  afv2orxorb  47177