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

Definition df-or 376
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 25927). After we define the constant true T. (df-tru 1458) and the constant false F. (df-fal 1461), we will be able to prove these truth table values:  ( ( T.  \/ T.  )  <-> T.  ) (truortru 1481), 
( ( T.  \/ F.  )  <-> T.  ) (truorfal 1482), 
( ( F.  \/ T.  )  <-> T.  ) (falortru 1483), and  ( ( F.  \/ F.  )  <-> F.  ) (falorfal 1484).

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  ( -.  ph  ->  ps ) for  ( ph  \/  ps ), we end up with an instance of previously proved theorem biid 244. This is the justification for the definition, along with the fact that it introduces a new symbol  \/. Contrast with  /\ (df-an 377), 
-> (wi 4),  -/\ (df-nan 1395), and  \/_ (df-xor 1416) . (Contributed by NM, 27-Dec-1992.)

Assertion
Ref Expression
df-or  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wo 374 . 2  wff  ( ph  \/  ps )
41wn 3 . . 3  wff  -.  ph
54, 2wi 4 . 2  wff  ( -. 
ph  ->  ps )
63, 5wb 189 1  wff  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
Colors of variables: wff setvar class
This definition is referenced by:  pm4.64  378  pm2.53  379  pm2.54  380  ori  381  orri  382  ord  383  imor  418  mtord  670  orbi2d  713  orimdi  863  ordi  880  pm5.17  904  pm5.6  928  orbidi  948  nanbi  1403  nanbiOLD  1404  cador  1522  19.43  1756  19.32v  1800  nfor  2029  19.32  2058  dfsb3  2214  sbor  2238  neor  2727  r19.30  2947  r19.32v  2948  r19.43  2958  dfif2  3895  disjor  4403  sotric  4803  sotrieq  4804  isso2i  4809  soxp  6941  unxpwdom2  8134  cflim2  8724  cfpwsdom  9040  ltapr  9501  ltxrlt  9735  isprm4  14689  euclemma  14720  islpi  20220  restntr  20253  alexsubALTlem2  21118  alexsubALTlem3  21119  2bornot2b  25957  disjorf  28243  funcnv5mpt  28324  ballotlemodife  29380  3orit  30397  dfon2lem5  30483  ecase13d  31019  elicc3  31023  nn0prpw  31029  bj-nf4  31240  onsucuni3  31816  orfa  32361  unitresl  32364  cnf1dd  32372  tsim1  32418  ifpidg  36181  ifpim123g  36190  ifpororb  36195  ifpor123g  36198  dfxor4  36404  df3or2  36406  frege83  36588  dffrege99  36604  frege131  36636  frege133  36638  pm10.541  36761  xrssre  37646  elprn2  37800  iundjiun  38403  r19.32  38723
  Copyright terms: Public domain W3C validator