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 402), ∨ (df-or 862), → (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 used 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  had0  1634  elsymdifxor  4206  sadadd2lem2  16600  f1omvdco3  19643  bj-bixor  37431  wl-df3xor2  38360  wl-3xorbi  38364  wl-2xor  38374  tsxo3  39039  tsxo4  39040  oneptri  44217  ifpxorxorb  44470  or3or  44982  axorbtnotaiffb  47917  axorbciffatcxorb  47919  aisbnaxb  47925  abnotbtaxb  47929  abnotataxb  47930  afv2orxorb  48242