Definition df-or 859

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 30625). After we define the constant true ⊤ (df-tru 1565) and the constant false ⊥ (df-fal 1575), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1599), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1600), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1601), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1602).

Contrast with ∧ (df-an 400), → (wi 4), ⊼ (df-nan 1514), and ⊻ (df-xor 1534). (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 858	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 208	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  860  pm2.53  862  pm2.54  863  imor  864  ori  872  orri  873  ord  875  orbi2d  926  orimdi  941  orbidi  965  pm5.6  1015  ordi  1019  pm5.17  1025  nanbi  1522  cador  1630  nf4  1809  19.43  1904  nfor  1926  19.32v  1962  19.32  2270  sbor  2342  dfsb3  2527  neor  3051  r19.43  3132  r19.32v  3197  dfif2  4484  disjor  5084  soxp  8111  unxpwdom2  9538  cflim2  10222  cfpwsdom  10544  ltapr  11005  ltxrlt  11255  isprm4  16720  euclemma  16750  dvdszzq  16758  isdomn5  20762  islpi  23211  restntr  23244  alexsubALTlem2  24110  alexsubALTlem3  24111  elplng  28989  plngcplem  28994  plngrotlem2  28997  2bornot2b  30668  disjorf  32781  funcnv5mpt  32871  cycpm2tr  33301  ballotlemodife  34797  orbi2iALT  36040  3orit  36071  dfon2lem5  36140  ecase13d  36678  elicc3  36682  nn0prpw  36688  onsucuni3  37866  orfa  38586  cnf1dd  38594  tsim1  38634  ineleq  38858  aks4d1p7  42705  safesnsupfilb  43999  ifpidg  44072  ifpim123g  44081  ifpororb  44086  ifpor123g  44089  dfxor4  44347  df3or2  44349  frege83  44527  dffrege99  44543  frege131  44575  frege133  44577  pm10.541  44948  xrssre  45929  iundjiun  47039  r19.32  47697