Theorem adantlr 468

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
adantlr	|- ( ( ( ph /\ th ) /\ ps ) -> ch )

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		simpl 108	. 2 |- ( ( ph /\ th ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 281	1 |- ( ( ( ph /\ th ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2antrr  479  ad2ant2r  500  ad2ant2rl  502  adantl3r  503  ad4ant14  505  ad4ant24  507  ad5ant13  510  ad5ant14  511  ad5ant15  512  3ad2antl1  1143  3ad2antl2  1144  ad4ant124  1194  3adant1r  1209  bilukdc  1374  intab  3800  pofun  4234  ralxfrd  4383  rexxfrd  4384  ordtri2or2exmidlem  4441  wessep  4492  poinxp  4608  relop  4689  fun11iun  5388  ssimaex  5482  fndmdif  5525  fconst2g  5635  foeqcnvco  5691  f1eqcocnv  5692  isocnv  5712  isocnv2  5713  riota2df  5750  grprinvd  5966  grpridd  5967  f1o2ndf1  6125  tfr1onlembacc  6239  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllembacc  6252  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  tfrcl  6261  xpdom2  6725  fimax2gtrilemstep  6794  xpfi  6818  eqsupti  6883  ordiso2  6920  enumctlemm  6999  mulcanpig  7143  prarloclemlt  7301  genpdf  7316  genpdisj  7331  addnqprl  7337  addnqpru  7338  addlocpr  7344  prmuloc  7374  mulnqprl  7376  mulnqpru  7377  mullocpr  7379  ltpopr  7403  ltsopr  7404  ltaddpr  7405  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  ltaprg  7427  recexprlemopu  7435  recexprlemloc  7439  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  caucvgsrlemcau  7601  caucvgsrlemgt1  7603  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  suplocsrlem  7616  axcaucvglemcau  7706  axpre-suploclemres  7709  axsuploc  7837  cnegexlem1  7937  cnegexlem3  7939  cnegex  7940  addsubeq4  7977  rimul  8347  divcanap6  8479  ltmul12a  8618  lemul12b  8619  lbinf  8706  zrevaddcl  9104  nzadd  9106  zextle  9142  fzind  9166  uz11  9348  qreccl  9434  qrevaddcl  9436  irradd  9438  xrlttr  9581  xrltso  9582  xaddass  9652  xleadd1a  9656  xlt2add  9663  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  divelunit  9785  uzsubsubfz  9827  fzaddel  9839  fzrev  9864  elfzmlbp  9909  frec2uzrdg  10182  frecuzrdgtcl  10185  frecuzrdgsuc  10187  frecuzrdgdomlem  10190  frecuzrdgfunlem  10192  frecuzrdgsuctlem  10196  iseqovex  10229  seq3val  10231  seqf  10234  seq3clss  10240  seq3fveq2  10242  seq3feq2  10243  seq3feq  10245  seq3shft2  10246  ser3mono  10251  seq3split  10252  seq3caopr3  10254  seq3caopr2  10255  iseqf1olemab  10262  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1olemstep  10274  seq3f1oleml  10276  seq3id3  10280  seq3id  10281  seq3id2  10282  seq3homo  10283  seq3z  10284  seqfeq3  10285  ser3ge0  10290  expp1  10300  expnegap0  10301  expcllem  10304  mulexp  10332  expadd  10335  expaddzap  10337  expmulzap  10339  expdivap  10344  leexp1a  10348  expnlbnd  10416  bcpasc  10512  bccl  10513  hashfacen  10579  seq3coll  10585  seq3shft  10610  resqrexlemfp1  10781  sqrtdiv  10814  climshftlemg  11071  climcn1  11077  climsqz  11104  climsqz2  11105  clim2ser  11106  clim2ser2  11107  isermulc2  11109  climub  11113  serf0  11121  fsum3cvg  11147  sumrbdc  11148  summodclem3  11149  summodclem2a  11150  zsumdc  11153  fsumf1o  11159  isumss  11160  fisumss  11161  isumss2  11162  fsum3cvg2  11163  fsum3cvg3  11165  fsumcl2lem  11167  fsumcllem  11168  fsumadd  11175  fsumsplit  11176  fsumsplitsn  11179  sumsplitdc  11201  fisumrev2  11215  fsum2mul  11222  fsum00  11231  telfsumo  11235  fsumparts  11239  iserabs  11244  cvgratnnlemabsle  11296  cvgratnn  11300  cvgratz  11301  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  clim2prod  11308  clim2divap  11309  prodfap0  11314  prodfrecap  11315  prodeq2  11326  fproddccvg  11341  prodrbdclem2  11342  prodmodc  11347  eftlcvg  11393  negdvdsb  11509  dvdsnegb  11510  dvdsext  11553  addmodlteqALT  11557  nno  11603  infssuzex  11642  gcdsupex  11646  gcdsupcl  11647  bezoutlembz  11692  dvdssq  11719  eucalgf  11736  dvdslcm  11750  lcmledvds  11751  lcmeq0  11752  lcmcl  11753  lcmdvds  11760  lcmgcdeq  11764  divgcdcoprmex  11783  phibndlem  11892  phiprmpw  11898  ctiunctlemf  11951  ctiunct  11953  opnssneib  12325  neissex  12334  tgrest  12338  iscnp3  12372  cnpnei  12388  cnrest  12404  tx1cn  12438  txcnp  12440  elbl3ps  12563  elbl3  12564  blininf  12593  blssexps  12598  blssex  12599  blpnfctr  12608  mopni2  12652  blsscls2  12662  metss  12663  bdmet  12671  metrest  12675  metcn  12683  txmetcn  12688  bl2ioo  12711  ivthinclemlr  12784  ivthinclemur  12786  dvcj  12842  dvfre  12843  coseq0q4123  12915  abssinper  12927  subctctexmid  13196  cvgcmp2n  13228