Definition df-xor 1541

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 1572) and the constant false ⊥ (df-fal 1582), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1614), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1615), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1616), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1617). Contrast with ∧ (df-an 402), ∨ (df-or 862), → (wi 4), and ⊼ (df-nan 1521). (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 1540	. 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 used by:  xnor  1542  xorcom  1543  xorass  1544  excxor  1545  xor2  1546  xorneg2  1550  xorbi12i  1553  xorbi12d  1554  anxordi  1555  xorexmid  1556  truxortru  1614  truxorfal  1615  falxorfal  1617  hadbi  1627  had0  1633  elsymdifxor  4205  sadadd2lem2  16625  f1omvdco3  19668  bj-bixor  37553  wl-df3xor2  38485  wl-3xorbi  38489  wl-2xor  38499  tsxo3  39164  tsxo4  39165  oneptri  44352  ifpxorxorb  44605  or3or  45116  axorbtnotaiffb  48066  axorbciffatcxorb  48068  aisbnaxb  48074  abnotbtaxb  48078  abnotataxb  48079  afv2orxorb  48391