Theorem adantlr 477

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 109	. 2 |- ( ( ph /\ th ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 283	1 |- ( ( ( ph /\ th ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  ad2antrr  488  ad2ant2r  509  ad2ant2rl  511  adantl3r  512  ad4ant14  514  ad4ant24  516  ad5ant13  519  ad5ant14  520  ad5ant15  521  3ad2antl1  1185  3ad2antl2  1186  ad4ant124  1242  3adant1r  1257  ad5ant235  1264  ad5ant135  1269  bilukdc  1440  elpr2elpr  3859  intab  3957  pofun  4409  ralxfrd  4559  rexxfrd  4560  ordtri2or2exmidlem  4624  wessep  4676  poinxp  4795  relop  4880  fun11iun  5604  ssimaex  5707  fndmdif  5752  fconst2g  5869  foeqcnvco  5931  f1eqcocnv  5932  isocnv  5952  isocnv2  5953  riota2df  5993  caofdig  6269  f1o2ndf1  6393  tfr1onlembacc  6508  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllembacc  6521  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  tfrcl  6530  xpdom2  7015  fimax2gtrilemstep  7090  xpfi  7124  eqsupti  7195  ordiso2  7234  enumctlemm  7313  enwomnilem  7368  cc2lem  7485  mulcanpig  7555  prarloclemlt  7713  genpdf  7728  genpdisj  7743  addnqprl  7749  addnqpru  7750  addlocpr  7756  prmuloc  7786  mulnqprl  7788  mulnqpru  7789  mullocpr  7791  ltpopr  7815  ltsopr  7816  ltaddpr  7817  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprg  7839  recexprlemopu  7847  recexprlemloc  7851  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  suplocsrlem  8028  axcaucvglemcau  8118  axpre-suploclemres  8121  axsuploc  8252  cnegexlem1  8354  cnegexlem3  8356  cnegex  8357  addsubeq4  8394  rimul  8765  divcanap6  8899  ltmul12a  9040  lemul12b  9041  lbinf  9128  zrevaddcl  9530  nzadd  9532  zextle  9571  fzind  9595  uz11  9779  infregelbex  9832  qreccl  9876  qrevaddcl  9878  irradd  9880  xrlttr  10030  xrltso  10031  xaddass  10104  xleadd1a  10108  xlt2add  10115  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  divelunit  10237  uzsubsubfz  10282  fzaddel  10294  fzrev  10319  elfzmlbp  10367  infssuzex  10494  zsupssdc  10499  frec2uzrdg  10672  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgdomlem  10680  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  iseqovex  10721  seq3val  10723  seqf  10727  seq3clss  10734  seq3fveq2  10738  seq3feq2  10739  seq3feq  10743  seq3shft2  10744  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemab  10765  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1oleml  10779  seqf1oglem2a  10781  seqf1oglem2  10783  seq3id3  10787  seq3id  10788  seq3id2  10789  seq3homo  10790  seq3z  10791  seqfeq3  10792  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  expp1  10809  expnegap0  10810  expcllem  10813  mulexp  10841  expadd  10844  expaddzap  10846  expmulzap  10848  expdivap  10853  leexp1a  10857  expnlbnd  10927  bcpasc  11029  bccl  11030  hashfacen  11101  seq3coll  11107  ccatlen  11176  ccatvalfn  11182  ccatsymb  11183  ccatalpha  11194  pfxclz  11264  wrd2ind  11308  swrdccat  11320  seq3shft  11403  resqrexlemfp1  11574  sqrtdiv  11607  climshftlemg  11867  climcn1  11873  climsqz  11900  climsqz2  11901  clim2ser  11902  clim2ser2  11903  isermulc2  11905  climub  11909  serf0  11917  fsum3cvg  11944  sumrbdc  11945  summodclem3  11946  summodclem2a  11947  zsumdc  11950  fsumf1o  11956  isumss  11957  fisumss  11958  isumss2  11959  fsum3cvg2  11960  fsum3cvg3  11962  fsumcl2lem  11964  fsumcllem  11965  fsumadd  11972  fsumsplit  11973  fsumsplitsn  11976  sumsplitdc  11998  fisumrev2  12012  fsum2mul  12019  fsum00  12028  telfsumo  12032  fsumparts  12036  iserabs  12041  cvgratnnlemabsle  12093  cvgratnn  12097  cvgratz  12098  mertenslemub  12100  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  clim2prod  12105  clim2divap  12106  prodfap0  12111  prodfrecap  12112  prodeq2  12123  fproddccvg  12138  prodrbdclem2  12139  prodmodc  12144  zproddc  12145  fprodf1o  12154  fprodssdc  12156  fprodunsn  12170  fprodcllem  12172  fprodabs  12182  fprodeq0  12183  fprodmodd  12207  eftlcvg  12253  negdvdsb  12373  dvdsnegb  12374  fsumdvds  12408  dvdsext  12421  addmodlteqALT  12425  nno  12472  gcdsupex  12533  gcdsupcl  12534  bezoutlembz  12580  dvdssq  12607  eucalgf  12632  dvdslcm  12646  lcmledvds  12647  lcmeq0  12648  lcmcl  12649  lcmdvds  12656  lcmgcdeq  12660  divgcdcoprmex  12679  isprm5lem  12718  phibndlem  12793  phiprmpw  12799  pc2dvds  12908  pcmpt  12921  prmpwdvds  12933  1arith  12945  4sqleminfi  12975  ctiunctlemf  13064  ctiunct  13066  grpinva  13474  grprida  13475  gsumpropd2  13481  sgrppropd  13501  prdssgrpd  13503  mndpropd  13528  prdsidlem  13535  prdsmndd  13536  mhmpropd  13554  0mhm  13574  resmhm2  13576  resmhm2b  13577  grplcan  13650  mulgval  13714  mulgnn0z  13741  mulgnndir  13743  mulgnn0dir  13744  issubg2m  13781  issubg4m  13785  subgintm  13790  ghmf1  13865  gsumfzmptfidmadd  13931  gsumfzmhm  13935  srglmhm  14012  srgrmhm  14013  ringpropd  14057  crngpropd  14058  ringlghm  14080  ringrghm  14081  mulgass3  14104  issubrng2  14230  subrngpropd  14236  issubrg2  14261  subrgintm  14263  subrgpropd  14273  rhmpropd  14274  unitrrg  14287  lmodprop2d  14368  islss3  14399  lssintclm  14404  qusrhm  14548  gsumfzfsum  14608  opnssneib  14886  neissex  14895  tgrest  14899  iscnp3  14933  cnpnei  14949  cnrest  14965  tx1cn  14999  txcnp  15001  elbl3ps  15124  elbl3  15125  blininf  15154  blssexps  15159  blssex  15160  blpnfctr  15169  mopni2  15213  blsscls2  15223  metss  15224  bdmet  15232  metrest  15236  metcn  15244  txmetcn  15249  bl2ioo  15280  ivthinclemlr  15367  ivthinclemur  15369  dvcj  15439  dvfre  15440  elplyd  15471  plyaddlem1  15477  plymullem1  15478  plymullem  15480  plycolemc  15488  plycjlemc  15490  coseq0q4123  15564  abssinper  15576  fsumdvdsmul  15721  lgsval2lem  15745  lgsval4lem  15746  lgsneg  15759  lgsmod  15761  lgsdir2  15768  lgsdir  15770  lgsne0  15773  lgssq  15775  lgsquadlem1  15812  usgredg2vlem2  16080  clwwlkccat  16258  clwwlknonex2lem2  16295  subctctexmid  16627  cvgcmp2n  16663  iswomninnlem  16679  nconstwlpo  16696