MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-or Structured version   Visualization version   GIF version

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

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 250. 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 1440), and (df-xor 1457) . (Contributed by NM, 27-Dec-1992.)

Assertion
Ref Expression
df-or ((𝜑𝜓) ↔ (¬ 𝜑𝜓))

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wo 382 . 2 wff (𝜑𝜓)
41wn 3 . . 3 wff ¬ 𝜑
54, 2wi 4 . 2 wff 𝜑𝜓)
63, 5wb 195 1 wff ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
This definition is referenced by:  pm4.64  386  pm2.53  387  pm2.54  388  ori  389  orri  390  ord  391  imor  427  mtord  690  orbi2d  734  orimdi  888  ordi  904  pm5.17  928  pm5.6  949  orbidi  969  nanbi  1446  cador  1538  nf4  1704  19.43  1799  nfor  1822  19.32v  1856  19.32  2088  nforOLD  2232  dfsb3  2362  sbor  2386  neor  2873  r19.30  3063  r19.32v  3064  r19.43  3074  dfif2  4038  disjor  4567  soxp  7177  unxpwdom2  8376  cflim2  8968  cfpwsdom  9285  ltapr  9746  ltxrlt  9987  isprm4  15235  euclemma  15263  islpi  20763  restntr  20796  alexsubALTlem2  21662  alexsubALTlem3  21663  2bornot2b  26712  disjorf  28774  funcnv5mpt  28852  ballotlemodife  29886  3orit  30851  dfon2lem5  30936  ecase13d  31477  elicc3  31481  nn0prpw  31488  bj-nf4  31768  onsucuni3  32391  orfa  33051  unitresl  33054  cnf1dd  33062  tsim1  33107  ifpidg  36855  ifpim123g  36864  ifpororb  36869  ifpor123g  36872  dfxor4  37077  df3or2  37079  frege83  37260  dffrege99  37276  frege131  37308  frege133  37310  pm10.541  37588  xrssre  38505  elprn2  38701  iundjiun  39353  r19.32  39816
  Copyright terms: Public domain W3C validator