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  1948  mooran2  2171  euor2  2184  undif3  3390  undif4  3472  ordelinel  4449  ordssun  4450  ordequn  4451  frxp  6145  omopth2  6536  swoord1  6643  swoord2  6644  sucprcreg  7267  rankxplim3  7505  fpwwe2lem12  8217  ltapr  8623  zmulcl  10019  elnn1uz2  10247  mnflt  10417  mnfltpnf  10418  expeq0  11084  vdwlem9  12984  funcres2c  13723  tsrlemax  14277  odlem1  14798  gexlem1  14838  0top  16669  cmpfi  17083  alexsubALTlem3  17691  dyadmbl  18903  plydivex  19625  scvxcvx  20228  dfon2lem4  23497  sltsgn1  23669  sltsgn2  23670  dfrdg4  23849  broutsideof2  24106  lineunray  24131  meran1  24211  facrm  24305  nxtor  24337  partarelt1  25249  prtlem90  26076  19.33-2  26933  stoweidlem26  27096  stoweidlem37  27107  a9e2ndeq  27362  undif3VD  27692  a9e2ndeqVD  27719  a9e2ndeqALT  27742  paddclN  29182  lcfl6  30841
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