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  8464  cnegexlem3  8466  cnegex  8467  addsubeq4  8504  rimul  8876  divcanap6  9010  ltmul12a  9151  lemul12b  9152  lbinf  9239  zrevaddcl  9645  nzadd  9647  zextle  9687  fzind  9711  uz11  9895  infregelbex  9948  qreccl  9992  qrevaddcl  9994  irradd  9996  xrlttr  10147  xrltso  10148  xaddass  10221  xleadd1a  10225  xlt2add  10232  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  divelunit  10354  uzsubsubfz  10401  fzaddel  10414  fzrev  10440  elfzmlbp  10488  infssuzex  10615  zsupssdc  10622  frec2uzrdg  10795  frecuzrdgtcl  10798  frecuzrdgsuc  10800  frecuzrdgdomlem  10803  frecuzrdgfunlem  10805  frecuzrdgsuctlem  10809  iseqovex  10844  seq3val  10846  seqf  10850  seq3clss  10857  seq3fveq2  10861  seq3feq2  10862  seq3feq  10866  seq3shft2  10867  ser3mono  10873  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemab  10888  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1oleml  10902  seqf1oglem2a  10904  seqf1oglem2  10906  seq3id3  10910  seq3id  10911  seq3id2  10912  seq3homo  10913  seq3z  10914  seqfeq3  10915  seqhomog  10916  seqfeq4g  10917  ser3ge0  10922  expp1  10932  expnegap0  10933  expcllem  10936  mulexp  10964  expadd  10967  expaddzap  10969  expmulzap  10971  expdivap  10976  leexp1a  10980  expnlbnd  11051  bcpasc  11153  bccl  11154  hashfacen  11233  seq3coll  11239  ccatlen  11308  ccatvalfn  11314  ccatsymb  11315  ccatalpha  11326  pfxclz  11396  wrd2ind  11440  swrdccat  11452  seq3shft  11548  resqrexlemfp1  11719  sqrtdiv  11752  climshftlemg  12012  climcn1  12018  climsqz  12045  climsqz2  12046  clim2ser  12047  clim2ser2  12048  isermulc2  12050  climub  12054  serf0  12062  fsum3cvg  12089  sumrbdc  12090  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsumf1o  12101  isumss  12102  fisumss  12103  isumss2  12104  fsum3cvg2  12105  fsum3cvg3  12107  fsumcl2lem  12109  fsumcllem  12110  fsumadd  12117  fsumsplit  12118  fsumsplitsn  12121  sumsplitdc  12143  fisumrev2  12157  fsum2mul  12164  fsum00  12173  telfsumo  12177  fsumparts  12181  iserabs  12186  cvgratnnlemabsle  12238  cvgratnn  12242  cvgratz  12243  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2prod  12250  clim2divap  12251  prodfap0  12256  prodfrecap  12257  prodeq2  12268  fproddccvg  12283  prodrbdclem2  12284  prodmodc  12289  zproddc  12290  fprodf1o  12299  fprodssdc  12301  fprodunsn  12315  fprodcllem  12317  fprodabs  12327  fprodeq0  12328  fprodmodd  12352  eftlcvg  12398  negdvdsb  12518  dvdsnegb  12519  fsumdvds  12553  dvdsext  12566  addmodlteqALT  12570  nno  12617  gcdsupex  12678  gcdsupcl  12679  bezoutlembz  12725  dvdssq  12752  eucalgf  12777  dvdslcm  12791  lcmledvds  12792  lcmeq0  12793  lcmcl  12794  lcmdvds  12801  lcmgcdeq  12805  divgcdcoprmex  12824  isprm5lem  12863  phibndlem  12938  phiprmpw  12944  pc2dvds  13053  pcmpt  13066  prmpwdvds  13078  1arith  13090  4sqleminfi  13120  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsv  13197  ballotfilemsima  13203  ctiunctlemf  13273  ctiunct  13275  grpinva  13683  grprida  13684  gsumpropd2  13690  sgrppropd  13710  prdssgrpd  13712  mndpropd  13737  prdsidlem  13744  prdsmndd  13745  mhmpropd  13763  0mhm  13783  resmhm2  13785  resmhm2b  13786  grplcan  13859  mulgval  13923  mulgnn0z  13950  mulgnndir  13952  mulgnn0dir  13953  issubg2m  13990  issubg4m  13994  subgintm  13999  ghmf1  14074  gsumfzmptfidmadd  14140  gsumfzmhm  14144  srglmhm  14221  srgrmhm  14222  ringpropd  14266  crngpropd  14267  ringlghm  14289  ringrghm  14290  mulgass3  14314  issubrng2  14441  subrngpropd  14447  issubrg2  14472  subrgintm  14474  subrgpropd  14484  rhmpropd  14485  unitrrg  14499  lmodprop2d  14608  islss3  14639  lssintclm  14644  qusrhm  14788  gsumfzfsum  14848  opnssneib  15133  neissex  15142  tgrest  15146  iscnp3  15180  cnpnei  15196  cnrest  15212  tx1cn  15246  txcnp  15248  elbl3ps  15371  elbl3  15372  blininf  15401  blssexps  15406  blssex  15407  blpnfctr  15416  mopni2  15460  blsscls2  15470  metss  15471  bdmet  15479  metrest  15483  metcn  15491  txmetcn  15496  bl2ioo  15527  ivthinclemlr  15614  ivthinclemur  15616  dvcj  15686  dvfre  15687  elplyd  15718  plyaddlem1  15724  plymullem1  15725  plymullem  15727  plycolemc  15735  plycjlemc  15737  coseq0q4123  15811  abssinper  15823  fsumdvdsmul  15971  lgsval2lem  15995  lgsval4lem  15996  lgsneg  16009  lgsmod  16011  lgsdir2  16018  lgsdir  16020  lgsne0  16023  lgssq  16025  lgsquadlem1  16062  usgredg2vlem2  16330  clwwlkccat  16508  clwwlknonex2lem2  16545  subctctexmid  16886  cvgcmp2n  16929  iswomninnlem  16946  nconstwlpo  16964