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

Definition df-or 359
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 20808). After we define the constant true  T. (df-tru 1310) and the constant false  F. (df-fal 1311), we will be able to prove these truth table values:  ( (  T.  \/  T.  )  <->  T.  ) (truortru 1330), 
( (  T.  \/  F.  )  <->  T.  ) (truorfal 1331), 
( (  F.  \/  T.  )  <->  T.  ) (falortru 1332), and  ( (  F.  \/  F.  )  <->  F.  ) (falorfal 1333).

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 227. This is the justification for the definition, along with the fact that it introduces a new symbol  \/. Contrast with  /\ (df-an 360), 
-> (wi 4),  -/\ (df-nan 1288), and  \/_ (df-xor 1296) . (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 357 . 2  wff  ( ph  \/  ps )
41wn 3 . . 3  wff  -.  ph
54, 2wi 4 . 2  wff  ( -. 
ph  ->  ps )
63, 5wb 176 1  wff  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
Colors of variables: wff set class
This definition is referenced by:  pm4.64  361  pm2.53  362  pm2.54  363  ori  364  orri  365  ord  366  imor  401  mtord  641  orbi2d  682  orimdi  820  ordi  834  pm5.17  858  pm5.6  878  orbidi  898  cador  1381  cadan  1382  19.30  1591  19.43  1592  nfor  1770  19.32  1811  dfsb3  1996  sbor  2006  neor  2530  r19.30  2685  r19.32v  2686  r19.43  2695  dfif2  3567  disjor  4007  sotric  4340  sotrieq  4341  isso2i  4346  soxp  6228  unxpwdom2  7302  cflim2  7889  cfpwsdom  8206  ltapr  8669  ltxrlt  8893  isprm4  12768  euclemma  12787  islpi  16880  restntr  16912  alexsubALTlem2  17742  alexsubALTlem3  17743  2bornot2b  20837  ballotlemodife  23056  funcnv5mpt  23236  disjorf  23356  3orit  24066  dfon2lem5  24143  nxtor  24985  ecase13d  26222  elicc3  26228  nn0prpw  26239  pm10.541  27562  fmul01lt1lem1  27714  stoweidlem34  27783  stoweidlem35  27784  r19.32  27945
  Copyright terms: Public domain W3C validator