Definition df-xor 1514

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 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1587), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1588), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1589), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1590). Contrast with ∧ (df-an 396), ∨ (df-or 849), → (wi 4), and ⊼ (df-nan 1494). (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 1513	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 206	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1515  xorcom  1516  xorass  1517  excxor  1518  xor2  1519  xorneg2  1523  xorbi12i  1526  xorbi12d  1527  anxordi  1528  xorexmid  1529  truxortru  1587  truxorfal  1588  falxorfal  1590  hadbi  1600  elsymdifxor  4214  sadadd2lem2  16389  f1omvdco3  19390  bj-bixor  36812  wl-df3xor2  37718  wl-3xorbi  37722  wl-2xor  37732  tsxo3  38384  tsxo4  38385  oneptri  43608  ifpxorxorb  43861  or3or  44373  axorbtnotaiffb  47257  axorbciffatcxorb  47259  aisbnaxb  47265  abnotbtaxb  47269  abnotataxb  47270  afv2orxorb  47582