Definition df-or 848

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 30357). After we define the constant true ⊤ (df-tru 1543) and the constant false ⊥ (df-fal 1553), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1577), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1578), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1579), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1580).

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1492), and ⊻ (df-xor 1512). (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 847	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  849  pm2.53  851  pm2.54  852  imor  853  ori  861  orri  862  ord  864  orbi2d  915  orimdi  930  orbidi  954  pm5.6  1003  ordi  1007  pm5.17  1013  nanbi  1500  cador  1608  nf4  1787  19.43  1882  nfor  1904  19.32v  1940  19.32  2234  sbor  2306  dfsb3  2493  neor  3018  r19.43  3102  r19.32v  3171  dfif2  4493  disjor  5092  soxp  8111  unxpwdom2  9548  cflim2  10223  cfpwsdom  10544  ltapr  11005  ltxrlt  11251  isprm4  16661  euclemma  16690  dvdszzq  16698  isdomn5  20626  islpi  23043  restntr  23076  alexsubALTlem2  23942  alexsubALTlem3  23943  2bornot2b  30400  disjorf  32515  funcnv5mpt  32599  cycpm2tr  33083  ballotlemodife  34496  orbi2iALT  35679  3orit  35710  dfon2lem5  35782  ecase13d  36308  elicc3  36312  nn0prpw  36318  onsucuni3  37362  orfa  38083  cnf1dd  38091  tsim1  38131  ineleq  38343  aks4d1p7  42078  safesnsupfilb  43414  ifpidg  43487  ifpim123g  43496  ifpororb  43501  ifpor123g  43504  dfxor4  43762  df3or2  43764  frege83  43942  dffrege99  43958  frege131  43990  frege133  43992  pm10.541  44363  xrssre  45351  elprn2  45639  iundjiun  46465  r19.32  47103