Theorem olcd 735

Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
orcd.1	|- ( ph -> ps )

Assertion

Ref	Expression
olcd	|- ( ph -> ( ch \/ ps ) )

Proof of Theorem olcd

Step	Hyp	Ref	Expression
1		orcd.1	. . 3 |- ( ph -> ps )
2	1	orcd 734	. 2 |- ( ph -> ( ps \/ ch ) )
3	2	orcomd 730	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  742  pm2.49  743  orim12i  760  pm1.5  766  animorr  825  animorlr  826  dcor  937  dcfrompeirce  1460  dcun  3561  exmidn0m  4235  regexmidlem1  4570  reg2exmidlema  4571  nn0suc  4641  nndceq0  4655  acexmidlem1  5921  nntri3or  6560  nntri2or2  6565  nndceq  6566  nndcel  6567  nnm00  6597  ssfilem  6945  diffitest  6957  tridc  6969  finexdc  6972  fientri3  6985  unsnfidcex  6990  unsnfidcel  6991  fidcenumlemrks  7028  fidcenumlemrk  7029  nninfisollemne  7206  nninfisol  7208  finomni  7215  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  exmidontriimlem2  7305  netap  7337  2omotaplemap  7340  mullocprlem  7654  recexprlemloc  7715  gt0ap0  8670  ltap  8677  recexaplem2  8696  nn1m1nn  9025  nn1gt1  9041  ltpnf  9872  mnflt  9875  xrltso  9888  xnn0dcle  9894  xnn0letri  9895  xrpnfdc  9934  xrmnfdc  9935  exfzdc  10333  infssuzex  10340  apbtwnz  10381  expnnval  10651  exp0  10652  bc0k  10865  bcpasc  10875  xrmaxadd  11443  sumdc  11540  zsumdc  11566  fsum3  11569  fisumss  11574  isumss2  11575  fsumsplit  11589  zproddc  11761  fprodseq  11765  fprodssdc  11772  fprodsplitdc  11778  fprodsplit  11779  fprodunsn  11786  fprodcl2lem  11787  fsumdvds  12024  pclemdc  12482  pcxqcl  12506  sumhashdc  12541  1arith  12561  4sqlem17  12601  ctiunctlemudc  12679  lringuplu  13828  suplociccreex  14944  plymullem1  15068  lgsdir2lem5  15357  djurclALT  15532  bj-nn0suc0  15680  trilpolemres  15773  trirec0  15775  nconstwlpolem  15796