MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-or Unicode 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 20737). After we define the constant true  T. (df-tru 1315) and the constant false  F. (df-fal 1316), we will be able to prove these truth table values:  ( (  T.  \/  T.  )  <->  T.  ) (truortru 1336), 
( (  T.  \/  F.  )  <->  T.  ) (truorfal 1337), 
( (  F.  \/  T.  )  <->  T.  ) (falortru 1338), and  ( (  F.  \/  F.  )  <->  F.  ) (falorfal 1339).

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

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 359 . 2  wff  ( ph  \/  ps )
41wn 5 . . 3  wff  -.  ph
54, 2wi 6 . 2  wff  ( -. 
ph  ->  ps )
63, 5wb 178 1  wff  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
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  644  orbi2d  685  orimdi  823  ordi  837  pm5.17  863  pm5.6  883  orbidi  903  cador  1387  cadan  1388  19.30  1603  19.43  1604  nfor  1736  19.32  1794  dfsb3  1949  sbor  1959  neor  2503  r19.30  2658  r19.32v  2659  r19.43  2668  dfif2  3527  disjor  3967  sotric  4298  sotrieq  4299  isso2i  4304  soxp  6148  unxpwdom2  7256  cflim2  7843  cfpwsdom  8160  ltapr  8623  ltxrlt  8847  isprm4  12716  euclemma  12735  islpi  16828  restntr  16860  alexsubALTlem2  17690  alexsubALTlem3  17691  2bornot2b  20783  ballotlemodife  23003  3orit  23424  dfon2lem5  23498  nxtor  24337  ecase13d  25575  elicc3  25581  nn0prpw  25592  pm10.541  26915  fmul01lt1lem1  27068  stoweidlem34  27104  stoweidlem35  27105
  Copyright terms: Public domain W3C validator