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

Theorem olc 375
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
olc  |-  ( ph  ->  ( ps  \/  ph ) )

Proof of Theorem olc
StepHypRef Expression
1 ax-1 7 . 2  |-  ( ph  ->  ( -.  ps  ->  ph ) )
21orrd 369 1  |-  ( ph  ->  ( ps  \/  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    \/ wo 359
This theorem is referenced by:  pm1.4  377  pm2.07  387  pm2.46  389  biorf  396  pm1.5  510  pm2.41  559  jaob  761  pm3.48  809  andi  842  pm4.72  851  dedlemb  926  consensus  930  cad1  1394  19.33  1606  19.33b  1607  dfsb2  1947  mooran2  2168  euor2  2181  undif3  3336  undif4  3418  ordssun  4383  ordequn  4384  frxp  6077  omopth2  6468  swoord1  6575  swoord2  6576  sucprcreg  7197  rankxplim3  7435  fpwwe2lem12  8143  ltapr  8549  zmulcl  9945  elnn1uz2  10173  mnflt  10343  mnfltpnf  10344  expeq0  11010  vdwlem9  12910  funcres2c  13619  tsrlemax  14164  odlem1  14685  gexlem1  14725  0top  16553  cmpfi  16967  alexsubALTlem3  17575  dyadmbl  18787  plydivex  19509  scvxcvx  20112  dfon2lem4  23310  sltsgn1  23482  sltsgn2  23483  dfrdg4  23662  broutsideof2  23919  lineunray  23944  meran1  24024  facrm  24118  nxtor  24150  partarelt1  25062  prtlem90  25889  19.33-2  26746  a9e2ndeq  27018  undif3VD  27348  a9e2ndeqVD  27375  a9e2ndeqALT  27398  paddclN  28720  lcfl6  30379
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator