Definition df-xor 1531

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 1562) and the constant false ⊥ (df-fal 1572), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1604), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1605), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1606), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1607). Contrast with ∧ (df-an 400), ∨ (df-or 859), → (wi 4), and ⊼ (df-nan 1511). (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 1530	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 208	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 208	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1532  xorcom  1533  xorass  1534  excxor  1535  xor2  1536  xorneg2  1540  xorbi12i  1543  xorbi12d  1544  anxordi  1545  xorexmid  1546  truxortru  1604  truxorfal  1605  falxorfal  1607  hadbi  1617  elsymdifxor  4212  sadadd2lem2  16467  f1omvdco3  19472  bj-bixor  36998  wl-df3xor2  37927  wl-3xorbi  37931  wl-2xor  37941  tsxo3  38602  tsxo4  38603  oneptri  43798  ifpxorxorb  44051  or3or  44563  axorbtnotaiffb  47461  axorbciffatcxorb  47463  aisbnaxb  47469  abnotbtaxb  47473  abnotataxb  47474  afv2orxorb  47786