Theorem olcd 742

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.48  749  pm2.49  750  orim12i  767  pm1.5  773  animorr  832  animorlr  833  dcor  944  dfifp2dc  990  dcfrompeirce  1495  dcun  3606  exmidn0m  4297  regexmidlem1  4637  reg2exmidlema  4638  nn0suc  4708  nndceq0  4722  acexmidlem1  6024  nntri3or  6704  nntri2or2  6709  nndceq  6710  nndcel  6711  nnm00  6741  ssfilem  7105  ssfilemd  7107  diffitest  7119  tridc  7132  finexdc  7135  elssdc  7137  eqsndc  7138  fientri3  7150  unsnfidcex  7155  unsnfidcel  7156  fidcenumlemrks  7195  fidcenumlemrk  7196  nninfisollemne  7390  nninfisol  7392  finomni  7399  pr1or2  7459  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidaclem  7483  exmidontriimlem2  7497  netap  7533  2omotaplemap  7536  mullocprlem  7850  recexprlemloc  7911  gt0ap0  8865  ltap  8872  recexaplem2  8891  nn1m1nn  9220  nn1gt1  9236  ltpnf  10076  mnflt  10079  xrltso  10092  xnn0dcle  10098  xnn0letri  10099  xrpnfdc  10138  xrmnfdc  10139  exfzdc  10549  infssuzex  10556  apbtwnz  10597  expnnval  10867  exp0  10868  bc0k  11081  bcpasc  11091  ccatsymb  11245  xrmaxadd  11901  sumdc  11998  zsumdc  12025  fsum3  12028  fisumss  12033  isumss2  12034  fsumsplit  12048  zproddc  12220  fprodseq  12224  fprodssdc  12231  fprodsplitdc  12237  fprodsplit  12238  fprodunsn  12245  fprodcl2lem  12246  fsumdvds  12483  pclemdc  12941  pcxqcl  12965  sumhashdc  13000  1arith  13020  4sqlem17  13060  ctiunctlemudc  13138  lringuplu  14291  suplociccreex  15435  plymullem1  15559  lgsdir2lem5  15851  upgr1een  16065  umgrvad2edg  16152  usgr1e  16182  eupth2lem2dc  16400  eupth2lem3lem4fi  16414  djurclALT  16520  bj-nn0suc0  16666  trilpolemres  16774  trirec0  16776  nconstwlpolem  16798