Theorem olcd 734

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

Syntax hints:   -> wi 4   \/ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  741  pm2.49  742  orim12i  759  pm1.5  765  animorr  824  animorlr  825  dcan  933  dcor  935  dcun  3534  exmidn0m  4202  regexmidlem1  4533  reg2exmidlema  4534  nn0suc  4604  nndceq0  4618  acexmidlem1  5871  nntri3or  6494  nntri2or2  6499  nndceq  6500  nndcel  6501  nnm00  6531  ssfilem  6875  diffitest  6887  tridc  6899  finexdc  6902  fientri3  6914  unsnfidcex  6919  unsnfidcel  6920  fidcenumlemrks  6952  fidcenumlemrk  6953  nninfisollemne  7129  nninfisol  7131  finomni  7138  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  exmidontriimlem2  7221  netap  7253  2omotaplemap  7256  mullocprlem  7569  recexprlemloc  7630  gt0ap0  8583  ltap  8590  recexaplem2  8609  nn1m1nn  8937  nn1gt1  8953  ltpnf  9780  mnflt  9783  xrltso  9796  xnn0dcle  9802  xnn0letri  9803  xrpnfdc  9842  xrmnfdc  9843  exfzdc  10240  apbtwnz  10274  expnnval  10523  exp0  10524  bc0k  10736  bcpasc  10746  xrmaxadd  11269  sumdc  11366  zsumdc  11392  fsum3  11395  fisumss  11400  isumss2  11401  fsumsplit  11415  zproddc  11587  fprodseq  11591  fprodssdc  11598  fprodsplitdc  11604  fprodsplit  11605  fprodunsn  11612  fprodcl2lem  11613  infssuzex  11950  pclemdc  12288  sumhashdc  12345  1arith  12365  ctiunctlemudc  12438  lringuplu  13337  suplociccreex  14105  lgsdir2lem5  14436  djurclALT  14557  bj-nn0suc0  14705  trilpolemres  14793  trirec0  14795  nconstwlpolem  14815