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

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1493), and ⊻ (df-xor 1513). (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  1501  cador  1609  nf4  1788  19.43  1883  nfor  1905  19.32v  1941  19.32  2238  sbor  2310  dfsb3  2496  neor  3021  r19.43  3101  r19.32v  3166  dfif2  4476  disjor  5075  soxp  8065  unxpwdom2  9481  cflim2  10161  cfpwsdom  10482  ltapr  10943  ltxrlt  11190  isprm4  16597  euclemma  16626  dvdszzq  16634  isdomn5  20627  islpi  23065  restntr  23098  alexsubALTlem2  23964  alexsubALTlem3  23965  2bornot2b  30446  disjorf  32561  funcnv5mpt  32652  cycpm2tr  33095  ballotlemodife  34532  orbi2iALT  35750  3orit  35781  dfon2lem5  35850  ecase13d  36378  elicc3  36382  nn0prpw  36388  onsucuni3  37432  orfa  38142  cnf1dd  38150  tsim1  38190  ineleq  38406  aks4d1p7  42196  safesnsupfilb  43535  ifpidg  43608  ifpim123g  43617  ifpororb  43622  ifpor123g  43625  dfxor4  43883  df3or2  43885  frege83  44063  dffrege99  44079  frege131  44111  frege133  44113  pm10.541  44484  xrssre  45471  iundjiun  46582  r19.32  47222