Definition df-or 855

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 30511). After we define the constant true ⊤ (df-tru 1551) and the constant false ⊥ (df-fal 1561), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1585), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1586), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1587), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1588).

Contrast with ∧ (df-an 398), → (wi 4), ⊼ (df-nan 1500), and ⊻ (df-xor 1520). (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 854	. 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  856  pm2.53  858  pm2.54  859  imor  860  ori  868  orri  869  ord  871  orbi2d  922  orimdi  937  orbidi  961  pm5.6  1010  ordi  1014  pm5.17  1020  nanbi  1508  cador  1616  nf4  1795  19.43  1890  nfor  1912  19.32v  1948  19.32  2247  sbor  2319  dfsb3  2504  neor  3028  r19.43  3109  r19.32v  3174  dfif2  4458  disjor  5056  soxp  8071  unxpwdom2  9497  cflim2  10181  cfpwsdom  10503  ltapr  10964  ltxrlt  11212  isprm4  16648  euclemma  16678  dvdszzq  16686  isdomn5  20685  islpi  23135  restntr  23168  alexsubALTlem2  24034  alexsubALTlem3  24035  2bornot2b  30554  disjorf  32670  funcnv5mpt  32761  cycpm2tr  33202  ballotlemodife  34692  orbi2iALT  35926  3orit  35957  dfon2lem5  36026  ecase13d  36554  elicc3  36558  nn0prpw  36564  onsucuni3  37742  orfa  38462  cnf1dd  38470  tsim1  38510  ineleq  38734  aks4d1p7  42581  safesnsupfilb  43875  ifpidg  43948  ifpim123g  43957  ifpororb  43962  ifpor123g  43965  dfxor4  44223  df3or2  44225  frege83  44403  dffrege99  44419  frege131  44451  frege133  44453  pm10.541  44824  xrssre  45805  iundjiun  46915  r19.32  47573