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 30449). After we define the constant true ⊤ (df-tru 1539) and the constant false ⊥ (df-fal 1549), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1573), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1574), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1575), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1576).

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1488), and ⊻ (df-xor 1508). (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  1496  cador  1604  nf4  1783  19.43  1879  nfor  1901  19.32v  1937  19.32  2230  sbor  2305  dfsb3  2496  neor  3031  r19.43  3119  r19.32v  3189  dfif2  4532  disjor  5129  soxp  8152  unxpwdom2  9625  cflim2  10300  cfpwsdom  10621  ltapr  11082  ltxrlt  11328  isprm4  16717  euclemma  16746  dvdszzq  16754  isdomn5  20726  islpi  23172  restntr  23205  alexsubALTlem2  24071  alexsubALTlem3  24072  2bornot2b  30492  disjorf  32598  funcnv5mpt  32684  cycpm2tr  33121  ballotlemodife  34478  orbi2iALT  35669  3orit  35695  dfon2lem5  35768  ecase13d  36295  elicc3  36299  nn0prpw  36305  onsucuni3  37349  orfa  38068  cnf1dd  38076  tsim1  38116  ineleq  38335  aks4d1p7  42064  safesnsupfilb  43407  ifpidg  43480  ifpim123g  43489  ifpororb  43494  ifpor123g  43497  dfxor4  43755  df3or2  43757  frege83  43935  dffrege99  43951  frege131  43983  frege133  43985  pm10.541  44362  xrssre  45297  elprn2  45589  iundjiun  46415  r19.32  47047