Definition df-or 383

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 26463). After we define the constant true ⊤ (df-tru 1477) and the constant false ⊥ (df-fal 1480), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1500), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1501), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1502), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1503).

This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute (¬ 𝜑 → 𝜓) for (𝜑 ∨ 𝜓), we end up with an instance of previously proved theorem biid 249. This is the justification for the definition, along with the fact that it introduces a new symbol ∨. Contrast with ∧ (df-an 384), → (wi 4), ⊼ (df-nan 1439), and ⊻ (df-xor 1456) . (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 381	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 194	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  385  pm2.53  386  pm2.54  387  ori  388  orri  389  ord  390  imor  426  mtord  689  orbi2d  733  orimdi  887  ordi  903  pm5.17  927  pm5.6  948  orbidi  968  nanbi  1445  cador  1537  nf4  1703  19.43  1798  nfor  1821  19.32v  1855  19.32  2087  nforOLD  2231  dfsb3  2361  sbor  2385  neor  2872  r19.30  3062  r19.32v  3063  r19.43  3073  dfif2  4037  disjor  4561  soxp  7154  unxpwdom2  8353  cflim2  8945  cfpwsdom  9262  ltapr  9723  ltxrlt  9959  isprm4  15183  euclemma  15211  islpi  20710  restntr  20743  alexsubALTlem2  21609  alexsubALTlem3  21610  2bornot2b  26505  disjorf  28567  funcnv5mpt  28645  ballotlemodife  29679  3orit  30644  dfon2lem5  30729  ecase13d  31270  elicc3  31274  nn0prpw  31281  bj-nf4  31561  onsucuni3  32174  orfa  32834  unitresl  32837  cnf1dd  32845  tsim1  32890  ifpidg  36638  ifpim123g  36647  ifpororb  36652  ifpor123g  36655  dfxor4  36860  df3or2  36862  frege83  37043  dffrege99  37059  frege131  37091  frege133  37093  pm10.541  37371  xrssre  38288  elprn2  38484  iundjiun  39136  r19.32  39599