Theorem olc 386

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

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

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 189  df-or 372

This theorem is referenced by:  pm1.4  388  pm2.07  398  pm2.46  400  biorf  407  pm1.5  525  pm2.41  577  jaob  792  pm3.48  844  norbi  870  andi  878  pm4.72  887  dedlemb  966  consensus  970  anifp  1433  cad1  1519  19.33  1747  19.33b  1748  dfsb2  2202  mooran2  2357  undif3  3704  undif4  3821  ordelinel  5521  ordssun  5522  ordequn  5523  tpres  6117  frxp  6906  omopth2  7285  swoord1  7392  swoord2  7393  rankxplim3  8352  fpwwe2lem12  9066  ltapr  9470  zmulcl  10985  nn0lt2  11000  elnn1uz2  11235  mnflt  11425  mnfltpnf  11428  fzm1  11874  expeq0  12302  vdwlem9  14939  cshwshashlem1  15066  cshwshash  15075  funcres2c  15806  tsrlemax  16466  odlem1  17181  odlem1OLD  17184  gexlem1  17228  gexlem1OLD  17230  0top  19999  cmpfi  20423  alexsubALTlem3  21064  dyadmbl  22558  plydivex  23250  scvxcvx  23911  nb3graprlem1  25179  uvtx01vtx  25220  1to3vfriswmgra  25735  frgraregorufr  25781  frgraregord13  25847  disjunsn  28204  dfon2lem4  30432  sltsgn1  30548  sltsgn2  30549  dfrdg4  30718  broutsideof2  30889  lineunray  30914  fwddifnp1  30932  meran1  31071  bj-falor2  31169  bj-nfntht  31196  bj-nfntht2  31197  bj-unrab  31529  wl-orel12  31849  tsor3  32391  prtlem90  32431  paddclN  33407  lcfl6  35068  ifpid3g  36136  ifpim4  36142  rp-fakeanorass  36157  iunrelexp0  36294  19.33-2  36731  ax6e2ndeq  36926  undif3VD  37279  ax6e2ndeqVD  37306  ax6e2ndeqALT  37328  disjxp1  37411  stoweidlem26  37886  stoweidlem37  37898  fourierswlem  38094  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  salexct  38193  sge0z  38217  nnfoctbdjlem  38293  nn0o1gt2ALTV  38823  stgoldbwt  38877  nb3grprlem1  39454  nrhmzr  39926  nn0o1gt2  40380