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 30350). 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  2492  neor  3017  r19.43  3101  r19.32v  3170  dfif2  4490  disjor  5089  soxp  8108  unxpwdom2  9541  cflim2  10216  cfpwsdom  10537  ltapr  10998  ltxrlt  11244  isprm4  16654  euclemma  16683  dvdszzq  16691  isdomn5  20619  islpi  23036  restntr  23069  alexsubALTlem2  23935  alexsubALTlem3  23936  2bornot2b  30393  disjorf  32508  funcnv5mpt  32592  cycpm2tr  33076  ballotlemodife  34489  orbi2iALT  35672  3orit  35703  dfon2lem5  35775  ecase13d  36301  elicc3  36305  nn0prpw  36311  onsucuni3  37355  orfa  38076  cnf1dd  38084  tsim1  38124  ineleq  38336  aks4d1p7  42071  safesnsupfilb  43407  ifpidg  43480  ifpim123g  43489  ifpororb  43494  ifpor123g  43497  dfxor4  43755  df3or2  43757  frege83  43935  dffrege99  43951  frege131  43983  frege133  43985  pm10.541  44356  xrssre  45344  elprn2  45632  iundjiun  46458  r19.32  47099