Definition df-or 385

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 27166). After we define the constant true ⊤ (df-tru 1483) and the constant false ⊥ (df-fal 1486), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1507), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1508), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1509), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1510).

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 251. This is the justification for the definition, along with the fact that it introduces a new symbol ∨. Contrast with ∧ (df-an 386), → (wi 4), ⊼ (df-nan 1445), and ⊻ (df-xor 1462) . (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 383	. 2 wff (𝜑 ∨ 𝜓)
4	1	wn 3	. . 3 wff ¬ 𝜑
5	4, 2	wi 4	. 2 wff (¬ 𝜑 → 𝜓)
6	3, 5	wb 196	1 wff ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))

This definition is referenced by:  pm4.64  387  pm2.53  388  pm2.54  389  ori  390  orri  391  ord  392  imor  428  mtord  691  orbi2d  737  orimdi  891  ordi  907  pm5.17  931  pm5.6  950  orbidi  972  nanbi  1451  cador  1544  nf4  1710  19.43  1807  nfor  1831  19.32v  1866  19.32  2099  nforOLD  2243  dfsb3  2373  sbor  2397  neor  2881  r19.30  3076  r19.32v  3077  r19.43  3087  dfif2  4066  disjor  4607  soxp  7250  unxpwdom2  8453  cflim2  9045  cfpwsdom  9366  ltapr  9827  ltxrlt  10068  isprm4  15340  euclemma  15368  islpi  20893  restntr  20926  alexsubALTlem2  21792  alexsubALTlem3  21793  2bornot2b  27208  disjorf  29278  funcnv5mpt  29353  ballotlemodife  30382  3orit  31358  dfon2lem5  31446  slttr2  31588  slttr3  31589  ecase13d  32002  elicc3  32006  nn0prpw  32013  onsucuni3  32886  orfa  33552  unitresl  33555  cnf1dd  33563  tsim1  33608  ifpidg  37356  ifpim123g  37365  ifpororb  37370  ifpor123g  37373  dfxor4  37578  df3or2  37580  frege83  37761  dffrege99  37777  frege131  37809  frege133  37811  pm10.541  38087  xrssre  39063  elprn2  39302  iundjiun  40014  r19.32  40501