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

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 1448), and ⊻ (df-xor 1465) . (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  692  orbi2d  738  orimdi  892  ordi  908  pm5.17  932  pm5.6  951  orbidi  973  nanbi  1454  cador  1547  nf4  1713  19.43  1810  nfor  1834  19.32v  1869  19.32  2101  nforOLD  2244  dfsb3  2374  sbor  2398  neor  2885  r19.30  3082  r19.32v  3083  r19.43  3093  dfif2  4088  disjor  4634  soxp  7290  unxpwdom2  8493  cflim2  9085  cfpwsdom  9406  ltapr  9867  ltxrlt  10108  isprm4  15397  euclemma  15425  islpi  20953  restntr  20986  alexsubALTlem2  21852  alexsubALTlem3  21853  2bornot2b  27320  disjorf  29392  funcnv5mpt  29469  ballotlemodife  30559  3orit  31596  dfon2lem5  31692  ecase13d  32307  elicc3  32311  nn0prpw  32318  onsucuni3  33215  orfa  33881  unitresl  33884  cnf1dd  33892  tsim1  33937  ineleq  34119  ifpidg  37836  ifpim123g  37845  ifpororb  37850  ifpor123g  37853  dfxor4  38058  df3or2  38060  frege83  38240  dffrege99  38256  frege131  38288  frege133  38290  pm10.541  38566  xrssre  39564  elprn2  39866  iundjiun  40677  r19.32  41167