Theorem olc 385

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

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 |- ( ph -> ( -. ps -> ph ) )
2	1	orrd 379	1 |- ( ph -> ( ps \/ ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188  df-or 371

This theorem is referenced by:  pm1.4  387  pm2.07  397  pm2.46  399  biorf  406  pm1.5  524  pm2.41  575  jaob  790  pm3.48  841  norbi  867  andi  875  pm4.72  884  dedlemb  963  consensus  967  anifp  1428  cad1  1514  19.33  1739  19.33b  1740  dfsb2  2165  mooran2  2322  undif3  3731  undif4  3846  ordelinel  5531  ordssun  5532  ordequn  5533  tpres  6123  frxp  6908  omopth2  7284  swoord1  7391  swoord2  7392  rankxplim3  8342  fpwwe2lem12  9055  ltapr  9459  zmulcl  10974  nn0lt2  10989  elnn1uz2  11224  mnflt  11414  mnfltpnf  11417  fzm1  11861  expeq0  12288  vdwlem9  14891  cshwshashlem1  15018  cshwshash  15027  funcres2c  15750  tsrlemax  16410  odlem1  17119  gexlem1  17159  0top  19923  cmpfi  20347  alexsubALTlem3  20988  dyadmbl  22432  plydivex  23115  scvxcvx  23773  nb3graprlem1  25021  uvtx01vtx  25062  1to3vfriswmgra  25577  frgraregorufr  25623  frgraregord13  25689  disjunsn  28040  dfon2lem4  30216  sltsgn1  30332  sltsgn2  30333  dfrdg4  30500  broutsideof2  30671  lineunray  30696  fwddifnp1  30714  meran1  30853  bj-falor2  30950  bj-nfntht  30975  bj-nfntht2  30976  bj-unrab  31276  wl-orel12  31553  tsor3  32095  prtlem90  32137  paddclN  33116  lcfl6  34777  ifpid3g  35839  ifpim4  35845  rp-fakeanorass  35860  iunrelexp0  35937  19.33-2  36372  ax6e2ndeq  36567  undif3VD  36923  ax6e2ndeqVD  36950  ax6e2ndeqALT  36972  stoweidlem26  37459  stoweidlem37  37471  fourierswlem  37666  fouriersw  37667  elaa2lem  37669  sge0z  37755  nnfoctbdjlem  37806  nn0o1gt2ALTV  38226  stgoldbwt  38280  nrhmzr  38644  nn0o1gt2  39101