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

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  1614  nf4  1794  19.43  1889  nfor  1911  19.32v  1947  19.32  2230  sbor  2308  dfsb3  2500  neor  3038  r19.32v  3270  r19.43  3280  dfif2  4467  disjor  5059  soxp  7961  unxpwdom2  9325  cflim2  10020  cfpwsdom  10341  ltapr  10802  ltxrlt  11046  isprm4  16387  euclemma  16416  islpi  22298  restntr  22331  alexsubALTlem2  23197  alexsubALTlem3  23198  2bornot2b  28824  disjorf  30914  funcnv5mpt  31001  dvdszzq  31125  cycpm2tr  31382  ballotlemodife  32460  3orit  33654  dfon2lem5  33759  ecase13d  34498  elicc3  34502  nn0prpw  34508  onsucuni3  35534  orfa  36236  cnf1dd  36244  tsim1  36284  ineleq  36482  aks4d1p7  40088  isdomn5  40168  ifpidg  41077  ifpim123g  41086  ifpororb  41091  ifpor123g  41094  dfxor4  41344  df3or2  41346  frege83  41524  dffrege99  41540  frege131  41572  frege133  41574  pm10.541  41955  xrssre  42858  elprn2  43146  iundjiun  43969  r19.32  44558