Definition df-xor 1512

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 1543) and the constant false ⊥ (df-fal 1553), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1585), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1586), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1587), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1588). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (wi 4), and ⊼ (df-nan 1492). (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 1511	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 206	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1513  xorcom  1514  xorass  1515  excxor  1516  xor2  1517  xorneg2  1521  xorbi12i  1524  xorbi12d  1525  anxordi  1526  xorexmid  1527  truxortru  1585  truxorfal  1586  falxorfal  1588  hadbi  1598  elsymdifxor  4240  sadadd2lem2  16474  f1omvdco3  19435  bj-bixor  36614  wl-df3xor2  37492  wl-3xorbi  37496  wl-2xor  37506  tsxo3  38168  tsxo4  38169  oneptri  43256  ifpxorxorb  43510  or3or  44022  axorbtnotaiffb  46912  axorbciffatcxorb  46914  aisbnaxb  46920  abnotbtaxb  46924  abnotataxb  46925  afv2orxorb  47237