Theorem olc 384

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 378	1 |- ( ph -> ( ps \/ ph ) )

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

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 185  df-or 370

This theorem is referenced by:  pm1.4  386  pm2.07  396  pm2.46  398  biorf  405  pm1.5  519  pm2.41  568  jaob  774  pm3.48  822  norbi  848  andi  855  pm4.72  864  dedlemb  939  consensus  943  cad1  1443  19.33  1661  19.33b  1662  dfsb2  2061  euor2OLD  2308  mooran2  2326  undif3  3599  undif4  3723  ordelinel  4804  ordssun  4805  ordequn  4806  frxp  6671  omopth2  7011  swoord1  7118  swoord2  7119  sucprcregOLD  7803  rankxplim3  8076  fpwwe2lem12  8795  ltapr  9201  zmulcl  10680  elnn1uz2  10918  mnflt  11091  mnfltpnf  11093  expeq0  11877  vdwlem9  14032  cshwshashlem1  14104  cshwshash  14113  funcres2c  14793  tsrlemax  15372  odlem1  16017  gexlem1  16057  0top  18429  cmpfi  18852  alexsubALTlem3  19462  dyadmbl  20921  plydivex  21647  scvxcvx  22263  nb3graprlem1  23181  uvtx01vtx  23222  disjunsn  25759  dfon2lem4  27445  sltsgn1  27648  sltsgn2  27649  dfrdg4  27827  broutsideof2  27999  lineunray  28024  meran1  28104  tsan3  28795  tsor3  28801  prtlem90  28844  19.33-2  29476  stoweidlem26  29664  stoweidlem37  29675  nn0lt2  30029  1to3vfriswmgra  30442  frgraregorufr  30489  frgraregord13  30555  ax6e2ndeq  30966  undif3VD  31317  ax6e2ndeqVD  31344  ax6e2ndeqALT  31366  bj-nfntht  31795  bj-nfntht2  31796  bj-unrab  32012  paddclN  33056  lcfl6  34715