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  1186  3ad2antl2  1187  ad4ant124  1243  3adant1r  1258  ad5ant235  1265  ad5ant135  1270  bilukdc  1441  ifeqeqxdc  3673  elpr2elpr  3885  intab  3983  pofun  4438  ralxfrd  4588  rexxfrd  4589  ordtri2or2exmidlem  4653  wessep  4705  poinxp  4824  relop  4910  fun11iun  5640  ssimaex  5743  fndmdif  5788  fconst2g  5904  foeqcnvco  5969  f1eqcocnv  5970  isocnv  5990  isocnv2  5991  riota2df  6033  caofdig  6309  f1o2ndf1  6437  tfr1onlembacc  6586  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllembacc  6599  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  tfrcl  6608  xpdom2  7095  fimax2gtrilemstep  7171  xpfi  7205  eqsupti  7300  ordiso2  7339  enumctlemm  7418  enwomnilem  7473  cc2lem  7596  mulcanpig  7666  prarloclemlt  7824  genpdf  7839  genpdisj  7854  addnqprl  7860  addnqpru  7861  addlocpr  7867  prmuloc  7897  mulnqprl  7899  mulnqpru  7900  mullocpr  7902  ltpopr  7926  ltsopr  7927  ltaddpr  7928  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltaprg  7950  recexprlemopu  7958  recexprlemloc  7962  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  suplocsrlem  8139  axcaucvglemcau  8229  axpre-suploclemres  8232  axsuploc  8362  cnegexlem1  8465  cnegexlem3  8467  cnegex  8468  addsubeq4  8505  rimul  8877  divcanap6  9013  ltmul12a  9154  lemul12b  9155  lbinf  9242  zrevaddcl  9648  nzadd  9650  zextle  9690  fzind  9714  uz11  9898  infregelbex  9951  qreccl  9995  qrevaddcl  9997  irradd  9999  xrlttr  10150  xrltso  10151  xaddass  10224  xleadd1a  10228  xlt2add  10235  iccshftr  10349  iccshftl  10351  iccdil  10353  icccntr  10355  divelunit  10357  uzsubsubfz  10404  fzaddel  10417  fzrev  10443  elfzmlbp  10491  infssuzex  10618  zsupssdc  10625  frec2uzrdg  10798  frecuzrdgtcl  10801  frecuzrdgsuc  10803  frecuzrdgdomlem  10806  frecuzrdgfunlem  10808  frecuzrdgsuctlem  10812  iseqovex  10847  seq3val  10849  seqf  10853  seq3clss  10860  seq3fveq2  10864  seq3feq2  10865  seq3feq  10869  seq3shft2  10870  ser3mono  10876  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  seq3caopr2  10882  seqcaopr2g  10883  iseqf1olemab  10891  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  seq3f1olemstep  10903  seq3f1oleml  10905  seqf1oglem2a  10907  seqf1oglem2  10909  seq3id3  10913  seq3id  10914  seq3id2  10915  seq3homo  10916  seq3z  10917  seqfeq3  10918  seqhomog  10919  seqfeq4g  10920  ser3ge0  10925  expp1  10935  expnegap0  10936  expcllem  10939  mulexp  10967  expadd  10970  expaddzap  10972  expmulzap  10974  expdivap  10979  leexp1a  10983  expnlbnd  11054  bcpasc  11156  bccl  11157  hashfacen  11236  seq3coll  11242  ccatlen  11311  ccatvalfn  11317  ccatsymb  11318  ccatalpha  11329  pfxclz  11399  wrd2ind  11443  swrdccat  11455  seq3shft  11551  resqrexlemfp1  11723  sqrtdiv  11756  climshftlemg  12016  climcn1  12022  climsqz  12049  climsqz2  12050  clim2ser  12051  clim2ser2  12052  isermulc2  12054  climub  12058  serf0  12066  fsum3cvg  12093  sumrbdc  12094  summodclem3  12095  summodclem2a  12096  zsumdc  12099  fsumf1o  12105  isumss  12106  fisumss  12107  isumss2  12108  fsum3cvg2  12109  fsum3cvg3  12111  fsumcl2lem  12113  fsumcllem  12114  fsumadd  12121  fsumsplit  12122  fsumsplitsn  12125  sumsplitdc  12147  fisumrev2  12161  fsum2mul  12168  fsum00  12177  telfsumo  12181  fsumparts  12185  iserabs  12190  cvgratnnlemabsle  12242  cvgratnn  12246  cvgratz  12247  mertenslemub  12249  mertenslemi1  12250  mertenslem2  12251  mertensabs  12252  clim2prod  12254  clim2divap  12255  prodfap0  12260  prodfrecap  12261  prodeq2  12272  fproddccvg  12287  prodrbdclem2  12288  prodmodc  12293  zproddc  12294  fprodf1o  12303  fprodssdc  12305  fprodunsn  12319  fprodcllem  12321  fprodabs  12331  fprodeq0  12332  fprodmodd  12356  eftlcvg  12402  negdvdsb  12522  dvdsnegb  12523  fsumdvds  12557  dvdsext  12570  addmodlteqALT  12574  nno  12621  gcdsupex  12682  gcdsupcl  12683  bezoutlembz  12729  dvdssq  12756  eucalgf  12781  dvdslcm  12795  lcmledvds  12796  lcmeq0  12797  lcmcl  12798  lcmdvds  12805  lcmgcdeq  12809  divgcdcoprmex  12828  isprm5lem  12867  phibndlem  12942  phiprmpw  12948  pc2dvds  13057  pcmpt  13070  prmpwdvds  13082  1arith  13094  4sqleminfi  13124  ballotfilemic  13198  ballotfilem1c  13199  ballotfilemsv  13201  ballotfilemsima  13207  ctiunctlemf  13277  ctiunct  13279  grpinva  13653  grprida  13654  gsumpropd2  13660  sgrppropd  13680  mndpropd  13705  mhmpropd  13725  0mhm  13745  resmhm2  13747  resmhm2b  13748  grplcan  13821  mulgval  13879  mulgnn0z  13906  mulgnndir  13908  mulgnn0dir  13909  issubg2m  13946  issubg4m  13950  subgintm  13955  ghmf1  14030  gsumfzmptfidmadd  14096  gsumfzmhm  14100  prdssgrpd  14137  prdsidlem  14139  prdsmndd  14140  srglmhm  14240  srgrmhm  14241  ringpropd  14285  crngpropd  14286  ringlghm  14308  ringrghm  14309  mulgass3  14333  issubrng2  14460  subrngpropd  14466  issubrg2  14491  subrgintm  14493  subrgpropd  14503  rhmpropd  14504  unitrrg  14518  lmodprop2d  14626  islss3  14657  lssintclm  14662  qusrhm  14806  gsumfzfsum  14866  opnssneib  15151  neissex  15160  tgrest  15164  iscnp3  15198  cnpnei  15214  cnrest  15230  tx1cn  15264  txcnp  15266  elbl3ps  15389  elbl3  15390  blininf  15419  blssexps  15424  blssex  15425  blpnfctr  15434  mopni2  15478  blsscls2  15488  metss  15489  bdmet  15497  metrest  15501  metcn  15509  txmetcn  15514  bl2ioo  15545  ivthinclemlr  15632  ivthinclemur  15634  dvcj  15704  dvfre  15705  elplyd  15736  plyaddlem1  15742  plymullem1  15743  plymullem  15745  plycolemc  15753  plycjlemc  15755  coseq0q4123  15829  abssinper  15841  fsumdvdsmul  15989  lgsval2lem  16013  lgsval4lem  16014  lgsneg  16027  lgsmod  16029  lgsdir2  16036  lgsdir  16038  lgsne0  16041  lgssq  16043  lgsquadlem1  16080  usgredg2vlem2  16348  clwwlkccat  16526  clwwlknonex2lem2  16563  subctctexmid  16914  cvgcmp2n  16957  iswomninnlem  16974  nconstwlpo  16991