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 30496). 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  2240  sbor  2312  dfsb3  2498  neor  3024  r19.43  3104  r19.32v  3169  dfif2  4481  disjor  5080  soxp  8071  unxpwdom2  9493  cflim2  10173  cfpwsdom  10495  ltapr  10956  ltxrlt  11203  isprm4  16611  euclemma  16640  dvdszzq  16648  isdomn5  20643  islpi  23093  restntr  23126  alexsubALTlem2  23992  alexsubALTlem3  23993  2bornot2b  30539  disjorf  32654  funcnv5mpt  32746  cycpm2tr  33201  ballotlemodife  34655  orbi2iALT  35879  3orit  35910  dfon2lem5  35979  ecase13d  36507  elicc3  36511  nn0prpw  36517  onsucuni3  37572  orfa  38283  cnf1dd  38291  tsim1  38331  ineleq  38547  aks4d1p7  42337  safesnsupfilb  43659  ifpidg  43732  ifpim123g  43741  ifpororb  43746  ifpor123g  43749  dfxor4  44007  df3or2  44009  frege83  44187  dffrege99  44203  frege131  44235  frege133  44237  pm10.541  44608  xrssre  45593  iundjiun  46704  r19.32  47344