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

Theorem olc 373
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 5 . 2  |-  ( ph  ->  ( -.  ps  ->  ph ) )
21orrd 367 1  |-  ( ph  ->  ( ps  \/  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  pm1.4  375  pm2.07  385  pm2.46  387  biorf  394  pm1.5  508  pm2.41  556  jaob  758  pm3.48  806  andi  837  pm4.72  846  dedlemb  921  consensus  925  cad1  1388  19.33  1594  19.33b  1595  dfsb2  1995  mooran2  2198  euor2  2211  undif3  3429  undif4  3511  ordelinel  4491  ordssun  4492  ordequn  4493  frxp  6225  omopth2  6582  swoord1  6689  swoord2  6690  sucprcreg  7313  rankxplim3  7551  fpwwe2lem12  8263  ltapr  8669  zmulcl  10066  elnn1uz2  10294  mnflt  10464  mnfltpnf  10465  expeq0  11132  vdwlem9  13036  funcres2c  13775  tsrlemax  14329  odlem1  14850  gexlem1  14890  0top  16721  cmpfi  17135  alexsubALTlem3  17743  dyadmbl  18955  plydivex  19677  scvxcvx  20280  dfon2lem4  24142  sltsgn1  24315  sltsgn2  24316  dfrdg4  24488  broutsideof2  24745  lineunray  24770  meran1  24850  facrm  24953  nxtor  24985  partarelt1  25896  prtlem90  26723  19.33-2  27580  stoweidlem26  27775  stoweidlem37  27786  uvtx01vtx  28164  1to3vfriswmgra  28185  a9e2ndeq  28325  undif3VD  28658  a9e2ndeqVD  28685  a9e2ndeqALT  28708  paddclN  30031  lcfl6  31690
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator