Theorem olcd 736

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 735	. 2 |- ( ph -> ( ps \/ ch ) )
3	2	orcomd 731	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  743  pm2.49  744  orim12i  761  pm1.5  767  animorr  826  animorlr  827  dcor  938  dcfrompeirce  1469  dcun  3570  exmidn0m  4246  regexmidlem1  4582  reg2exmidlema  4583  nn0suc  4653  nndceq0  4667  acexmidlem1  5942  nntri3or  6581  nntri2or2  6586  nndceq  6587  nndcel  6588  nnm00  6618  ssfilem  6974  diffitest  6986  tridc  6998  finexdc  7001  fientri3  7014  unsnfidcex  7019  unsnfidcel  7020  fidcenumlemrks  7057  fidcenumlemrk  7058  nninfisollemne  7235  nninfisol  7237  finomni  7244  exmidfodomrlemeldju  7309  exmidfodomrlemreseldju  7310  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  exmidontriimlem2  7336  netap  7368  2omotaplemap  7371  mullocprlem  7685  recexprlemloc  7746  gt0ap0  8701  ltap  8708  recexaplem2  8727  nn1m1nn  9056  nn1gt1  9072  ltpnf  9904  mnflt  9907  xrltso  9920  xnn0dcle  9926  xnn0letri  9927  xrpnfdc  9966  xrmnfdc  9967  exfzdc  10371  infssuzex  10378  apbtwnz  10419  expnnval  10689  exp0  10690  bc0k  10903  bcpasc  10913  ccatsymb  11061  xrmaxadd  11605  sumdc  11702  zsumdc  11728  fsum3  11731  fisumss  11736  isumss2  11737  fsumsplit  11751  zproddc  11923  fprodseq  11927  fprodssdc  11934  fprodsplitdc  11940  fprodsplit  11941  fprodunsn  11948  fprodcl2lem  11949  fsumdvds  12186  pclemdc  12644  pcxqcl  12668  sumhashdc  12703  1arith  12723  4sqlem17  12763  ctiunctlemudc  12841  lringuplu  13991  suplociccreex  15129  plymullem1  15253  lgsdir2lem5  15542  djurclALT  15775  bj-nn0suc0  15923  trilpolemres  16018  trirec0  16020  nconstwlpolem  16041