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  3535  exmidn0m  4203  regexmidlem1  4534  reg2exmidlema  4535  nn0suc  4605  nndceq0  4619  acexmidlem1  5874  nntri3or  6497  nntri2or2  6502  nndceq  6503  nndcel  6504  nnm00  6534  ssfilem  6878  diffitest  6890  tridc  6902  finexdc  6905  fientri3  6917  unsnfidcex  6922  unsnfidcel  6923  fidcenumlemrks  6955  fidcenumlemrk  6956  nninfisollemne  7132  nninfisol  7134  finomni  7141  exmidfodomrlemeldju  7201  exmidfodomrlemreseldju  7202  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  exmidaclem  7210  exmidontriimlem2  7224  netap  7256  2omotaplemap  7259  mullocprlem  7572  recexprlemloc  7633  gt0ap0  8586  ltap  8593  recexaplem2  8612  nn1m1nn  8940  nn1gt1  8956  ltpnf  9783  mnflt  9786  xrltso  9799  xnn0dcle  9805  xnn0letri  9806  xrpnfdc  9845  xrmnfdc  9846  exfzdc  10243  apbtwnz  10277  expnnval  10526  exp0  10527  bc0k  10739  bcpasc  10749  xrmaxadd  11272  sumdc  11369  zsumdc  11395  fsum3  11398  fisumss  11403  isumss2  11404  fsumsplit  11418  zproddc  11590  fprodseq  11594  fprodssdc  11601  fprodsplitdc  11607  fprodsplit  11608  fprodunsn  11615  fprodcl2lem  11616  infssuzex  11953  pclemdc  12291  sumhashdc  12348  1arith  12368  ctiunctlemudc  12441  lringuplu  13343  suplociccreex  14242  lgsdir2lem5  14573  djurclALT  14694  bj-nn0suc0  14842  trilpolemres  14931  trirec0  14933  nconstwlpolem  14954