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  4245  regexmidlem1  4581  reg2exmidlema  4582  nn0suc  4652  nndceq0  4666  acexmidlem1  5940  nntri3or  6579  nntri2or2  6584  nndceq  6585  nndcel  6586  nnm00  6616  ssfilem  6972  diffitest  6984  tridc  6996  finexdc  6999  fientri3  7012  unsnfidcex  7017  unsnfidcel  7018  fidcenumlemrks  7055  fidcenumlemrk  7056  nninfisollemne  7233  nninfisol  7235  finomni  7242  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  exmidontriimlem2  7334  netap  7366  2omotaplemap  7369  mullocprlem  7683  recexprlemloc  7744  gt0ap0  8699  ltap  8706  recexaplem2  8725  nn1m1nn  9054  nn1gt1  9070  ltpnf  9902  mnflt  9905  xrltso  9918  xnn0dcle  9924  xnn0letri  9925  xrpnfdc  9964  xrmnfdc  9965  exfzdc  10369  infssuzex  10376  apbtwnz  10417  expnnval  10687  exp0  10688  bc0k  10901  bcpasc  10911  ccatsymb  11058  xrmaxadd  11572  sumdc  11669  zsumdc  11695  fsum3  11698  fisumss  11703  isumss2  11704  fsumsplit  11718  zproddc  11890  fprodseq  11894  fprodssdc  11901  fprodsplitdc  11907  fprodsplit  11908  fprodunsn  11915  fprodcl2lem  11916  fsumdvds  12153  pclemdc  12611  pcxqcl  12635  sumhashdc  12670  1arith  12690  4sqlem17  12730  ctiunctlemudc  12808  lringuplu  13958  suplociccreex  15096  plymullem1  15220  lgsdir2lem5  15509  djurclALT  15742  bj-nn0suc0  15890  trilpolemres  15985  trirec0  15987  nconstwlpolem  16008