Definition df-or 847

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 30224). After we define the constant true ⊤ (df-tru 1537) and the constant false ⊥ (df-fal 1547), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1571), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1572), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1573), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1574).

Contrast with ∧ (df-an 396), → (wi 4), ⊼ (df-nan 1486), and ⊻ (df-xor 1506). (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 846	. 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  848  pm2.53  850  pm2.54  851  imor  852  ori  860  orri  861  ord  863  orbi2d  914  orimdi  929  orbidi  951  pm5.6  1000  ordi  1004  pm5.17  1010  nanbi  1494  cador  1602  nf4  1782  19.43  1878  nfor  1900  19.32v  1936  19.32  2222  sbor  2297  dfsb3  2489  neor  3030  r19.43  3118  r19.32v  3187  dfif2  4526  disjor  5122  soxp  8128  unxpwdom2  9605  cflim2  10280  cfpwsdom  10601  ltapr  11062  ltxrlt  11308  isprm4  16648  euclemma  16677  dvdszzq  16686  isdomn5  21242  islpi  23046  restntr  23079  alexsubALTlem2  23945  alexsubALTlem3  23946  2bornot2b  30267  disjorf  32362  funcnv5mpt  32447  cycpm2tr  32834  ballotlemodife  34111  3orit  35304  dfon2lem5  35377  ecase13d  35791  elicc3  35795  nn0prpw  35801  onsucuni3  36840  orfa  37549  cnf1dd  37557  tsim1  37597  ineleq  37820  aks4d1p7  41548  safesnsupfilb  42842  ifpidg  42915  ifpim123g  42924  ifpororb  42929  ifpor123g  42932  dfxor4  43190  df3or2  43192  frege83  43370  dffrege99  43386  frege131  43418  frege133  43420  pm10.541  43798  xrssre  44724  elprn2  45016  iundjiun  45842  r19.32  46472