Definition df-xor 1542

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 1573) and the constant false ⊥ (df-fal 1583), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1615), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1616), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1617), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1618). Contrast with ∧ (df-an 401), ∨ (df-or 861), → (wi 4), and ⊼ (df-nan 1522). (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 1541	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 209	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 209	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1543  xorcom  1544  xorass  1545  excxor  1546  xor2  1547  xorneg2  1551  xorbi12i  1554  xorbi12d  1555  anxordi  1556  xorexmid  1557  truxortru  1615  truxorfal  1616  falxorfal  1618  hadbi  1628  elsymdifxor  4214  sadadd2lem2  16509  f1omvdco3  19520  bj-bixor  37162  wl-df3xor2  38093  wl-3xorbi  38097  wl-2xor  38107  tsxo3  38766  tsxo4  38767  oneptri  43964  ifpxorxorb  44217  or3or  44729  axorbtnotaiffb  47617  axorbciffatcxorb  47619  aisbnaxb  47625  abnotbtaxb  47629  abnotataxb  47630  afv2orxorb  47942