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  1183  3ad2antl2  1184  ad4ant124  1240  3adant1r  1255  ad5ant235  1262  ad5ant135  1267  bilukdc  1438  elpr2elpr  3853  intab  3951  pofun  4400  ralxfrd  4550  rexxfrd  4551  ordtri2or2exmidlem  4615  wessep  4667  poinxp  4785  relop  4869  fun11iun  5589  ssimaex  5688  fndmdif  5733  fconst2g  5847  foeqcnvco  5907  f1eqcocnv  5908  isocnv  5928  isocnv2  5929  riota2df  5969  caofdig  6242  f1o2ndf1  6364  tfr1onlembacc  6478  tfr1onlemaccex  6484  tfr1onlemres  6485  tfrcllembacc  6491  tfrcllemaccex  6497  tfrcllemres  6498  tfrcldm  6499  tfrcl  6500  xpdom2  6978  fimax2gtrilemstep  7050  xpfi  7082  eqsupti  7151  ordiso2  7190  enumctlemm  7269  enwomnilem  7324  cc2lem  7440  mulcanpig  7510  prarloclemlt  7668  genpdf  7683  genpdisj  7698  addnqprl  7704  addnqpru  7705  addlocpr  7711  prmuloc  7741  mulnqprl  7743  mulnqpru  7744  mullocpr  7746  ltpopr  7770  ltsopr  7771  ltaddpr  7772  ltexprlemdisj  7781  ltexprlemloc  7782  ltexprlemru  7787  addcanprleml  7789  addcanprlemu  7790  ltaprg  7794  recexprlemopu  7802  recexprlemloc  7806  cauappcvgprlemladdfl  7830  cauappcvgprlemladdru  7831  caucvgsrlemcau  7968  caucvgsrlemgt1  7970  caucvgsrlemoffcau  7973  caucvgsrlemoffres  7975  suplocsrlem  7983  axcaucvglemcau  8073  axpre-suploclemres  8076  axsuploc  8207  cnegexlem1  8309  cnegexlem3  8311  cnegex  8312  addsubeq4  8349  rimul  8720  divcanap6  8854  ltmul12a  8995  lemul12b  8996  lbinf  9083  zrevaddcl  9485  nzadd  9487  zextle  9526  fzind  9550  uz11  9733  infregelbex  9781  qreccl  9825  qrevaddcl  9827  irradd  9829  xrlttr  9979  xrltso  9980  xaddass  10053  xleadd1a  10057  xlt2add  10064  iccshftr  10178  iccshftl  10180  iccdil  10182  icccntr  10184  divelunit  10186  uzsubsubfz  10231  fzaddel  10243  fzrev  10268  elfzmlbp  10316  infssuzex  10440  zsupssdc  10445  frec2uzrdg  10618  frecuzrdgtcl  10621  frecuzrdgsuc  10623  frecuzrdgdomlem  10626  frecuzrdgfunlem  10628  frecuzrdgsuctlem  10632  iseqovex  10667  seq3val  10669  seqf  10673  seq3clss  10680  seq3fveq2  10684  seq3feq2  10685  seq3feq  10689  seq3shft2  10690  ser3mono  10696  seq3split  10697  seqsplitg  10698  seq3caopr3  10700  seq3caopr2  10702  seqcaopr2g  10703  iseqf1olemab  10711  seq3f1olemqsumkj  10720  seq3f1olemqsumk  10721  seq3f1olemqsum  10722  seq3f1olemstep  10723  seq3f1oleml  10725  seqf1oglem2a  10727  seqf1oglem2  10729  seq3id3  10733  seq3id  10734  seq3id2  10735  seq3homo  10736  seq3z  10737  seqfeq3  10738  seqhomog  10739  seqfeq4g  10740  ser3ge0  10745  expp1  10755  expnegap0  10756  expcllem  10759  mulexp  10787  expadd  10790  expaddzap  10792  expmulzap  10794  expdivap  10799  leexp1a  10803  expnlbnd  10873  bcpasc  10975  bccl  10976  hashfacen  11045  seq3coll  11051  ccatlen  11116  ccatvalfn  11122  ccatsymb  11123  pfxclz  11197  wrd2ind  11241  swrdccat  11253  seq3shft  11335  resqrexlemfp1  11506  sqrtdiv  11539  climshftlemg  11799  climcn1  11805  climsqz  11832  climsqz2  11833  clim2ser  11834  clim2ser2  11835  isermulc2  11837  climub  11841  serf0  11849  fsum3cvg  11875  sumrbdc  11876  summodclem3  11877  summodclem2a  11878  zsumdc  11881  fsumf1o  11887  isumss  11888  fisumss  11889  isumss2  11890  fsum3cvg2  11891  fsum3cvg3  11893  fsumcl2lem  11895  fsumcllem  11896  fsumadd  11903  fsumsplit  11904  fsumsplitsn  11907  sumsplitdc  11929  fisumrev2  11943  fsum2mul  11950  fsum00  11959  telfsumo  11963  fsumparts  11967  iserabs  11972  cvgratnnlemabsle  12024  cvgratnn  12028  cvgratz  12029  mertenslemub  12031  mertenslemi1  12032  mertenslem2  12033  mertensabs  12034  clim2prod  12036  clim2divap  12037  prodfap0  12042  prodfrecap  12043  prodeq2  12054  fproddccvg  12069  prodrbdclem2  12070  prodmodc  12075  zproddc  12076  fprodf1o  12085  fprodssdc  12087  fprodunsn  12101  fprodcllem  12103  fprodabs  12113  fprodeq0  12114  fprodmodd  12138  eftlcvg  12184  negdvdsb  12304  dvdsnegb  12305  fsumdvds  12339  dvdsext  12352  addmodlteqALT  12356  nno  12403  gcdsupex  12464  gcdsupcl  12465  bezoutlembz  12511  dvdssq  12538  eucalgf  12563  dvdslcm  12577  lcmledvds  12578  lcmeq0  12579  lcmcl  12580  lcmdvds  12587  lcmgcdeq  12591  divgcdcoprmex  12610  isprm5lem  12649  phibndlem  12724  phiprmpw  12730  pc2dvds  12839  pcmpt  12852  prmpwdvds  12864  1arith  12876  4sqleminfi  12906  ctiunctlemf  12995  ctiunct  12997  grpinva  13405  grprida  13406  gsumpropd2  13412  sgrppropd  13432  prdssgrpd  13434  mndpropd  13459  prdsidlem  13466  prdsmndd  13467  mhmpropd  13485  0mhm  13505  resmhm2  13507  resmhm2b  13508  grplcan  13581  mulgval  13645  mulgnn0z  13672  mulgnndir  13674  mulgnn0dir  13675  issubg2m  13712  issubg4m  13716  subgintm  13721  ghmf1  13796  gsumfzmptfidmadd  13862  gsumfzmhm  13866  srglmhm  13942  srgrmhm  13943  ringpropd  13987  crngpropd  13988  ringlghm  14010  ringrghm  14011  mulgass3  14034  issubrng2  14159  subrngpropd  14165  issubrg2  14190  subrgintm  14192  subrgpropd  14202  rhmpropd  14203  unitrrg  14216  lmodprop2d  14297  islss3  14328  lssintclm  14333  qusrhm  14477  gsumfzfsum  14537  opnssneib  14815  neissex  14824  tgrest  14828  iscnp3  14862  cnpnei  14878  cnrest  14894  tx1cn  14928  txcnp  14930  elbl3ps  15053  elbl3  15054  blininf  15083  blssexps  15088  blssex  15089  blpnfctr  15098  mopni2  15142  blsscls2  15152  metss  15153  bdmet  15161  metrest  15165  metcn  15173  txmetcn  15178  bl2ioo  15209  ivthinclemlr  15296  ivthinclemur  15298  dvcj  15368  dvfre  15369  elplyd  15400  plyaddlem1  15406  plymullem1  15407  plymullem  15409  plycolemc  15417  plycjlemc  15419  coseq0q4123  15493  abssinper  15505  fsumdvdsmul  15650  lgsval2lem  15674  lgsval4lem  15675  lgsneg  15688  lgsmod  15690  lgsdir2  15697  lgsdir  15699  lgsne0  15702  lgssq  15704  lgsquadlem1  15741  usgredg2vlem2  16006  subctctexmid  16297  cvgcmp2n  16332  iswomninnlem  16348  nconstwlpo  16365