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  4208  sadadd2lem2  16649  f1omvdco3  19693  bj-bixor  37639  wl-df3xor2  38584  wl-3xorbi  38588  wl-2xor  38598  tsxo3  39263  tsxo4  39264  oneptri  44451  ifpxorxorb  44704  or3or  45215  axorbtnotaiffb  48178  axorbciffatcxorb  48180  aisbnaxb  48186  abnotbtaxb  48190  abnotataxb  48191  afv2orxorb  48503