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  4216  sadadd2lem2  16533  f1omvdco3  19550  bj-bixor  37225  wl-df3xor2  38156  wl-3xorbi  38160  wl-2xor  38170  tsxo3  38829  tsxo4  38830  oneptri  44025  ifpxorxorb  44278  or3or  44790  axorbtnotaiffb  47681  axorbciffatcxorb  47683  aisbnaxb  47689  abnotbtaxb  47693  abnotataxb  47694  afv2orxorb  48006