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  dcun  3556  exmidn0m  4230  regexmidlem1  4565  reg2exmidlema  4566  nn0suc  4636  nndceq0  4650  acexmidlem1  5914  nntri3or  6546  nntri2or2  6551  nndceq  6552  nndcel  6553  nnm00  6583  ssfilem  6931  diffitest  6943  tridc  6955  finexdc  6958  fientri3  6971  unsnfidcex  6976  unsnfidcel  6977  fidcenumlemrks  7012  fidcenumlemrk  7013  nninfisollemne  7190  nninfisol  7192  finomni  7199  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  exmidontriimlem2  7282  netap  7314  2omotaplemap  7317  mullocprlem  7630  recexprlemloc  7691  gt0ap0  8645  ltap  8652  recexaplem2  8671  nn1m1nn  9000  nn1gt1  9016  ltpnf  9846  mnflt  9849  xrltso  9862  xnn0dcle  9868  xnn0letri  9869  xrpnfdc  9908  xrmnfdc  9909  exfzdc  10307  apbtwnz  10343  expnnval  10613  exp0  10614  bc0k  10827  bcpasc  10837  xrmaxadd  11404  sumdc  11501  zsumdc  11527  fsum3  11530  fisumss  11535  isumss2  11536  fsumsplit  11550  zproddc  11722  fprodseq  11726  fprodssdc  11733  fprodsplitdc  11739  fprodsplit  11740  fprodunsn  11747  fprodcl2lem  11748  infssuzex  12086  pclemdc  12426  pcxqcl  12450  sumhashdc  12485  1arith  12505  4sqlem17  12545  ctiunctlemudc  12594  lringuplu  13692  suplociccreex  14778  plymullem1  14894  lgsdir2lem5  15148  djurclALT  15294  bj-nn0suc0  15442  trilpolemres  15532  trirec0  15534  nconstwlpolem  15555