Definition df-xor 1640

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 1662) and the constant false ⊥ (df-fal 1672), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1704), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1705), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1706), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1707). Contrast with ∧ (df-an 387), ∨ (df-or 881), → (wi 4), and ⊼ (df-nan 1615). (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 1639	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 198	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 198	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1641  xorcom  1642  xorass  1643  excxor  1644  xor2  1645  xorneg2  1649  xorbi12i  1652  xorbi12d  1653  anxordi  1654  xorexmid  1655  truxortru  1704  truxorfal  1705  falxorfal  1707  hadbi  1713  elsymdifxor  4078  sadadd2lem2  15546  f1omvdco3  18220  tsxo3  34487  tsxo4  34488  ifpxorxorb  38699  or3or  39160  axorbtnotaiffb  41865  axorbciffatcxorb  41867  aisbnaxb  41873  abnotbtaxb  41877  abnotataxb  41878  afv2orxorb  42131