Definition df-or 845

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

Contrast with ∧ (df-an 397), → (wi 4), ⊼ (df-nan 1487), and ⊻ (df-xor 1507). (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 844	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  846  pm2.53  848  pm2.54  849  imor  850  ori  858  orri  859  ord  861  unitreslOLD  875  orbi2d  913  orimdi  928  orbidi  950  pm5.6  999  ordi  1003  pm5.17  1009  nanbi  1495  cador  1610  nf4  1790  19.43  1885  nfor  1907  19.32v  1943  19.32  2226  sbor  2304  dfsb3  2498  neor  3036  r19.32v  3270  r19.43  3280  dfif2  4461  disjor  5054  soxp  7970  unxpwdom2  9347  cflim2  10019  cfpwsdom  10340  ltapr  10801  ltxrlt  11045  isprm4  16389  euclemma  16418  islpi  22300  restntr  22333  alexsubALTlem2  23199  alexsubALTlem3  23200  2bornot2b  28828  disjorf  30918  funcnv5mpt  31005  dvdszzq  31129  cycpm2tr  31386  ballotlemodife  32464  3orit  33658  dfon2lem5  33763  ecase13d  34502  elicc3  34506  nn0prpw  34512  onsucuni3  35538  orfa  36240  cnf1dd  36248  tsim1  36288  ineleq  36486  aks4d1p7  40091  isdomn5  40171  ifpidg  41098  ifpim123g  41107  ifpororb  41112  ifpor123g  41115  dfxor4  41374  df3or2  41376  frege83  41554  dffrege99  41570  frege131  41602  frege133  41604  pm10.541  41985  xrssre  42887  elprn2  43175  iundjiun  43998  r19.32  44590