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  23553  sltsgn1  23726  sltsgn2  23727  dfrdg4  23899  broutsideof2  24156  lineunray  24181  meran1  24261  facrm  24365  nxtor  24397  partarelt1  25308  prtlem90  26135  19.33-2  26992  stoweidlem26  27187  stoweidlem37  27198  1to3vfriswmgra  27547  a9e2ndeq  27698  undif3VD  28031  a9e2ndeqVD  28058  a9e2ndeqALT  28081  paddclN  29404  lcfl6  31063
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