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  4209  sadadd2lem2  16546  f1omvdco3  19582  bj-bixor  37300  wl-df3xor2  38231  wl-3xorbi  38235  wl-2xor  38245  tsxo3  38895  tsxo4  38896  oneptri  44106  ifpxorxorb  44359  or3or  44871  axorbtnotaiffb  47799  axorbciffatcxorb  47801  aisbnaxb  47807  abnotbtaxb  47811  abnotataxb  47812  afv2orxorb  48124