Definition df-or 844

Description: Define disjunction (logical "or"). Definition of [Margaris] p. 49. When the left operand, right operand, or both are true, the result is true; when both sides are false, the result is false. For example, it is true that (2 = 3 ∨ 4 = 4) (ex-or 28200). After we define the constant true ⊤ (df-tru 1540) and the constant false ⊥ (df-fal 1550), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1574), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1575), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1576), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1577).

Contrast with ∧ (df-an 399), → (wi 4), ⊼ (df-nan 1482), and ⊻ (df-xor 1502). (Contributed by NM, 27-Dec-1992.)

Assertion

Ref	Expression
df-or	⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

Detailed syntax breakdown of Definition df-or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wo 843	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 208	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  845  pm2.53  847  pm2.54  848  imor  849  ori  857  orri  858  ord  860  unitreslOLD  874  orbi2d  912  orimdi  927  orbidi  949  pm5.6  998  ordi  1002  pm5.17  1008  nanbi  1490  cador  1609  nf4  1788  19.43  1883  nfor  1905  19.32v  1941  19.32  2235  sbor  2316  dfsb3  2533  dfsb3ALT  2592  neor  3108  r19.30OLD  3339  r19.32v  3340  r19.43  3351  dfif2  4469  disjor  5046  soxp  7823  unxpwdom2  9052  cflim2  9685  cfpwsdom  10006  ltapr  10467  ltxrlt  10711  isprm4  16028  euclemma  16057  islpi  21757  restntr  21790  alexsubALTlem2  22656  alexsubALTlem3  22657  2bornot2b  28243  disjorf  30329  funcnv5mpt  30413  dvdszzq  30531  cycpm2tr  30761  ballotlemodife  31755  3orit  32945  dfon2lem5  33032  ecase13d  33661  elicc3  33665  nn0prpw  33671  onsucuni3  34651  orfa  35375  cnf1dd  35383  tsim1  35423  ineleq  35623  ifpidg  39906  ifpim123g  39915  ifpororb  39920  ifpor123g  39923  dfxor4  40160  df3or2  40162  frege83  40341  dffrege99  40357  frege131  40389  frege133  40391  pm10.541  40748  xrssre  41665  elprn2  41964  iundjiun  42791  r19.32  43345