Definition df-or 384

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 27581). After we define the constant true ⊤ (df-tru 1627) and the constant false ⊥ (df-fal 1630), we will be able to prove these truth table values: ((⊤ ∨ ⊤) ↔ ⊤) (truortru 1651), ((⊤ ∨ ⊥) ↔ ⊤) (truorfal 1652), ((⊥ ∨ ⊤) ↔ ⊤) (falortru 1653), and ((⊥ ∨ ⊥) ↔ ⊥) (falorfal 1654).

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 385), → (wi 4), ⊼ (df-nan 1589), and ⊻ (df-xor 1606) . (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 382	. 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  386  pm2.53  387  pm2.54  388  ori  389  orri  390  ord  391  imor  427  mtord  695  orbi2d  740  orimdi  928  ordi  944  pm5.17  968  pm5.6  989  orbidi  1011  nanbi  1595  cador  1688  nf4  1854  19.43  1951  nfor  1975  19.32v  2010  19.32  2240  nforOLD  2381  dfsb3  2503  sbor  2527  neor  3015  r19.30  3212  r19.32v  3213  r19.43  3223  dfif2  4224  disjor  4778  soxp  7450  unxpwdom2  8650  cflim2  9269  cfpwsdom  9590  ltapr  10051  ltxrlt  10292  isprm4  15591  euclemma  15619  islpi  21147  restntr  21180  alexsubALTlem2  22045  alexsubALTlem3  22046  2bornot2b  27623  disjorf  29691  funcnv5mpt  29770  ballotlemodife  30860  3orit  31895  dfon2lem5  31989  ecase13d  32605  elicc3  32609  nn0prpw  32616  onsucuni3  33518  orfa  34186  unitresl  34189  cnf1dd  34197  tsim1  34242  ineleq  34434  ifpidg  38330  ifpim123g  38339  ifpororb  38344  ifpor123g  38347  dfxor4  38552  df3or2  38554  frege83  38734  dffrege99  38750  frege131  38782  frege133  38784  pm10.541  39060  xrssre  40054  elprn2  40361  iundjiun  41172  r19.32  41665