Definition df-xor 1465

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 1486) and the constant false ⊥ (df-fal 1489), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1528), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1529), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1530), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1531). Contrast with ∧ (df-an 386), ∨ (df-or 385), → (wi 4), and ⊼ (df-nan 1448) . (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 1464	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 196	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 196	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1466  xorcom  1467  xorass  1468  excxor  1469  xor2  1470  xorneg2  1474  xorbi12i  1477  xorbi12d  1478  anxordi  1479  xorexmid  1480  truxortru  1528  truxorfal  1529  falxorfal  1531  hadbi  1537  sadadd2lem2  15172  f1omvdco3  17869  tsxo3  33946  tsxo4  33947  ifpxorxorb  37856  or3or  38319  axorbtnotaiffb  41070  axorbciffatcxorb  41072  aisbnaxb  41078  abnotbtaxb  41082  abnotataxb  41083