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  3019  r19.43  3103  r19.32v  3172  dfif2  4498  disjor  5097  soxp  8117  unxpwdom2  9559  cflim2  10234  cfpwsdom  10555  ltapr  11016  ltxrlt  11262  isprm4  16660  euclemma  16689  dvdszzq  16697  isdomn5  20625  islpi  23042  restntr  23075  alexsubALTlem2  23941  alexsubALTlem3  23942  2bornot2b  30400  disjorf  32515  funcnv5mpt  32600  cycpm2tr  33084  ballotlemodife  34497  orbi2iALT  35674  3orit  35700  dfon2lem5  35772  ecase13d  36298  elicc3  36302  nn0prpw  36308  onsucuni3  37352  orfa  38073  cnf1dd  38081  tsim1  38121  ineleq  38339  aks4d1p7  42063  safesnsupfilb  43379  ifpidg  43452  ifpim123g  43461  ifpororb  43466  ifpor123g  43469  dfxor4  43727  df3or2  43729  frege83  43907  dffrege99  43923  frege131  43955  frege133  43957  pm10.541  44328  xrssre  45317  elprn2  45605  iundjiun  46431  r19.32  47069