Definition df-xor 1507

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 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1584), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1585), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1586), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1587). Contrast with ∧ (df-an 397), ∨ (df-or 845), → (wi 4), and ⊼ (df-nan 1487). (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 1506	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 205	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1508  xorcom  1509  xorcomOLD  1510  xorass  1511  excxor  1512  xor2  1513  xorneg2  1517  xorbi12i  1520  xorbi12iOLD  1521  xorbi12d  1522  anxordi  1523  xorexmid  1524  truxortru  1584  truxorfal  1585  falxorfal  1587  hadbi  1599  elsymdifxor  4183  sadadd2lem2  16157  f1omvdco3  19057  bj-bixor  34773  wl-df3xor2  35640  wl-3xorbi  35644  wl-2xor  35654  tsxo3  36297  tsxo4  36298  ifpxorxorb  41118  or3or  41631  axorbtnotaiffb  44398  axorbciffatcxorb  44400  aisbnaxb  44406  abnotbtaxb  44410  abnotataxb  44411  afv2orxorb  44720