Definition df-xor 1512

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 1543) and the constant false ⊥ (df-fal 1553), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1585), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1586), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1587), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1588). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1492). (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 1511	. 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  1513  xorcom  1514  xorass  1515  excxor  1516  xor2  1517  xorneg2  1521  xorbi12i  1524  xorbi12d  1525  anxordi  1526  xorexmid  1527  truxortru  1585  truxorfal  1586  falxorfal  1588  hadbi  1598  elsymdifxor  4235  sadadd2lem2  16467  f1omvdco3  19428  bj-bixor  36555  wl-df3xor2  37433  wl-3xorbi  37437  wl-2xor  37447  tsxo3  38109  tsxo4  38110  oneptri  43228  ifpxorxorb  43482  or3or  43994  axorbtnotaiffb  46880  axorbciffatcxorb  46882  aisbnaxb  46888  abnotbtaxb  46892  abnotataxb  46893  afv2orxorb  47205