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

Definition df-or 361
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 21861). After we define the constant true (df-tru 1334) and the constant false (df-fal 1335), we will be able to prove these truth table values: (( ⊤ ∨ ⊤ ) ↔ ⊤ ) (truortru 1355), (( ⊤ ∨ ⊥ ) ↔ ⊤ ) (truorfal 1356), (( ⊥ ∨ ⊤ ) ↔ ⊤ ) (falortru 1357), and (( ⊥ ∨ ⊥ ) ↔ ⊥ ) (falorfal 1358).

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 229. This is the justification for the definition, along with the fact that it introduces a new symbol . Contrast with (df-an 362), (wi 4), (df-nan 1302), and (df-xor 1319) . (Contributed by NM, 5-Aug-1993.)

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

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wo 359 . 2 wff (𝜑𝜓)
41wn 3 . . 3 wff ¬ 𝜑
54, 2wi 4 . 2 wff 𝜑𝜓)
63, 5wb 178 1 wff ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff set class
This definition is referenced by:  pm4.64  363  pm2.53  364  pm2.54  365  ori  366  orri  367  ord  368  imor  403  mtord  643  orbi2d  684  orimdi  822  ordi  836  pm5.17  860  pm5.6  880  orbidi  900  cador  1406  cadanOLD  1408  19.30  1624  19.43  1625  nfor  1869  19.32  1908  dfsb3  2126  sbor  2155  neor  2731  r19.30  2896  r19.32v  2897  r19.43  2907  dfif2  3811  disjor  4277  sotric  4621  sotrieq  4622  isso2i  4627  soxp  6563  unxpwdom2  7651  cflim2  8240  cfpwsdom  8556  ltapr  9019  ltxrlt  9243  isprm4  13209  euclemma  13228  islpi  17345  restntr  17378  alexsubALTlem2  18211  alexsubALTlem3  18212  2bornot2b  21890  disjorf  24163  funcnv5mpt  24233  fzocatel  24324  ballotlemodife  25148  sgn3da  25192  3orit  25629  dfon2lem5  25871  ecase13d  26772  elicc3  26776  nn0prpw  26782  orfa  27148  unitresl  27151  cnf1dd  27159  tsim1  27168  tsbi3  27173  pm10.541  28061  r19.32  28439  sborNEW7  30616  dfsb3NEW7  30689
  Copyright terms: Public domain W3C validator