Definition df-xor 1504

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 396), ∨ (df-or 844), → (wi 4), and ⊼ (df-nan 1484). (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 1503	. 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  1505  xorcom  1506  xorcomOLD  1507  xorass  1508  excxor  1509  xor2  1510  xorneg2  1514  xorbi12i  1517  xorbi12iOLD  1518  xorbi12d  1519  anxordi  1520  xorexmid  1521  truxortru  1584  truxorfal  1585  falxorfal  1587  hadbi  1600  elsymdifxor  4180  sadadd2lem2  16085  f1omvdco3  18972  bj-bixor  34700  wl-df3xor2  35567  wl-3xorbi  35571  wl-2xor  35581  tsxo3  36224  tsxo4  36225  ifpxorxorb  41016  or3or  41520  axorbtnotaiffb  44285  axorbciffatcxorb  44287  aisbnaxb  44293  abnotbtaxb  44297  abnotataxb  44298  afv2orxorb  44607