Theorem adantlr 481

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2antrr  492  ad2ant2r  513  ad2ant2rl  515  adantl3r  516  ad4ant14  518  ad4ant24  520  ad5ant13  523  ad5ant14  524  ad5ant15  525  3ad2antl1  1190  3ad2antl2  1191  ad4ant124  1247  3adant1r  1262  ad5ant235  1269  ad5ant135  1274  bilukdc  1445  ifeqeqxdc  3687  elpr2elpr  3901  intab  3999  pofun  4457  ralxfrd  4608  rexxfrd  4609  ordtri2or2exmidlem  4673  wessep  4725  poinxp  4844  relop  4930  fun11iun  5660  relndmfv  5728  ssimaex  5764  fndmdif  5814  fconst2g  5930  foeqcnvco  5996  f1eqcocnv  5997  isocnv  6017  isocnv2  6018  riota2df  6060  caofdig  6336  f1o2ndf1  6464  tfr1onlembacc  6613  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllembacc  6626  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfrcl  6635  xpdom2  7129  fimax2gtrilemstep  7205  xpfi  7239  eqsupti  7337  ordiso2  7376  enumctlemm  7455  enwomnilem  7510  cc2lem  7633  mulcanpig  7703  prarloclemlt  7861  genpdf  7876  genpdisj  7891  addnqprl  7897  addnqpru  7898  addlocpr  7904  prmuloc  7934  mulnqprl  7936  mulnqpru  7937  mullocpr  7939  ltpopr  7963  ltsopr  7964  ltaddpr  7965  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  ltaprg  7987  recexprlemopu  7995  recexprlemloc  7999  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  suplocsrlem  8176  axcaucvglemcau  8266  axpre-suploclemres  8269  axsuploc  8399  cnegexlem1  8503  cnegexlem3  8505  cnegex  8506  addsubeq4  8543  rimul  8916  divcanap6  9052  ltmul12a  9193  lemul12b  9194  lbinf  9281  zrevaddcl  9700  nzadd  9702  zextle  9742  fzind  9766  uz11  9955  infregelbex  10008  qreccl  10052  qrevaddcl  10054  irradd  10056  xrlttr  10208  xrltso  10209  xaddass  10282  xleadd1a  10286  xlt2add  10293  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  divelunit  10415  uzsubsubfz  10463  fzaddel  10476  fzrev  10502  elfzmlbp  10550  infssuzex  10677  zsupssdc  10684  frec2uzrdg  10860  frecuzrdgtcl  10863  frecuzrdgsuc  10865  frecuzrdgdomlem  10868  frecuzrdgfunlem  10870  frecuzrdgsuctlem  10874  iseqovex  10909  seq3val  10911  seqf  10915  seq3clss  10922  seq3fveq2  10926  seq3feq2  10927  seq3feq  10931  seq3shft2  10932  ser3mono  10938  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  seq3caopr2  10944  seqcaopr2g  10945  iseqf1olemab  10953  seq3f1olemqsumkj  10962  seq3f1olemqsumk  10963  seq3f1olemqsum  10964  seq3f1olemstep  10965  seq3f1oleml  10967  seqf1oglem2a  10969  seqf1oglem2  10971  seq3id3  10975  seq3id  10976  seq3id2  10977  seq3homo  10978  seq3z  10979  seqfeq3  10980  seqhomog  10981  seqfeq4g  10982  ser3ge0  10987  expp1  10997  expnegap0  10998  expcllem  11001  mulexp  11029  expadd  11032  expaddzap  11034  expmulzap  11036  expdivap  11041  leexp1a  11045  expnlbnd  11116  bcpasc  11219  bccl  11220  hashfacen  11299  seq3coll  11309  ccatlen  11378  ccatvalfn  11384  ccatsymb  11385  ccatalpha  11396  pfxclz  11466  wrd2ind  11510  swrdccat  11522  seq3shft  11618  resqrexlemfp1  11790  sqrtdiv  11823  climshftlemg  12086  climcn1  12092  climsqz  12119  climsqz2  12120  clim2ser  12121  clim2ser2  12122  isermulc2  12124  climub  12128  serf0  12136  fsum3cvg  12163  sumrbdc  12164  summodclem3  12165  summodclem2a  12166  zsumdc  12169  fsumf1o  12175  isumss  12176  fisumss  12177  isumss2  12178  fsum3cvg2  12179  fsum3cvg3  12181  fsumcl2lem  12183  fsumcllem  12184  fsumadd  12191  fsumsplit  12192  fsumsplitsn  12195  sumsplitdc  12217  fisumrev2  12231  fsum2mul  12238  fsum00  12247  telfsumo  12251  fsumparts  12255  iserabs  12260  cvgratnnlemabsle  12312  cvgratnn  12316  cvgratz  12317  mertenslemub  12319  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  clim2prod  12324  clim2divap  12325  prodfap0  12330  prodfrecap  12331  prodeq2  12342  fproddccvg  12357  prodrbdclem2  12358  prodmodc  12363  zproddc  12364  fprodf1o  12373  fprodssdc  12375  fprodunsn  12389  fprodcllem  12391  fprodabs  12401  fprodeq0  12402  fprodmodd  12426  eftlcvg  12472  negdvdsb  12592  dvdsnegb  12593  fsumdvds  12627  dvdsext  12640  addmodlteqALT  12644  nno  12691  gcdsupex  12752  gcdsupcl  12753  bezoutlembz  12799  dvdssq  12826  eucalgf  12851  dvdslcm  12865  lcmledvds  12866  lcmeq0  12867  lcmcl  12868  lcmdvds  12875  lcmgcdeq  12879  divgcdcoprmex  12898  isprm5lem  12938  phibndlem  13016  phiprmpw  13022  pc2dvds  13131  pcmpt  13144  prmpwdvds  13156  1arith  13168  4sqleminfi  13198  ballotfilemic  13301  ballotfilem1c  13302  ballotfilemsv  13304  ballotfilemsima  13310  ctiunctlemf  13380  ctiunct  13382  grpinva  13757  grprida  13758  sgrppropd  13779  mndpropd  13804  mhmpropd  13824  0mhm  13844  resmhm2  13846  resmhm2b  13847  grplcan  13918  mulgval  13976  mulgnn0z  14003  mulgnndir  14005  mulgnn0dir  14006  issubg2m  14043  issubg4m  14047  subgintm  14052  ghmf1  14127  gzsummhm  14196  gsumressfi  14218  prdssgrpd  14242  prdsidlem  14244  prdsmndd  14245  srglmhm  14348  srgrmhm  14349  ringpropd  14394  crngpropd  14395  ringlghm  14417  ringrghm  14418  mulgass3  14442  issubrng2  14569  subrngpropd  14575  issubrg2  14600  subrgintm  14602  subrgpropd  14612  rhmpropd  14613  unitrrg  14627  lmodprop2d  14736  islss3  14767  lssintclm  14772  qusrhm  14916  issubassa3  15063  opnssneib  15309  neissex  15318  tgrest  15322  iscnp3  15356  cnpnei  15372  cnrest  15388  tx1cn  15422  txcnp  15424  elbl3ps  15547  elbl3  15548  blininf  15577  blssexps  15582  blssex  15583  blpnfctr  15592  mopni2  15636  blsscls2  15646  metss  15647  bdmet  15655  metrest  15659  metcn  15667  txmetcn  15672  bl2ioo  15703  ivthinclemlr  15790  ivthinclemur  15792  dvcj  15862  dvfre  15863  elplyd  15894  plyaddlem1  15900  plymullem1  15901  plymullem  15903  plycolemc  15911  plycjlemc  15913  coseq0q4123  15988  abssinper  16000  fsumdvdsmul  16207  ppiqub  16215  bposlem5  16237  lgsval2lem  16251  lgsval4lem  16252  lgsneg  16265  lgsmod  16267  lgsdir2  16274  lgsdir  16276  lgsne0  16279  lgssq  16281  lgsquadlem1  16318  usgredg2vlem2  16586  clwwlkccat  16764  clwwlknonex2lem2  16801  subctctexmid  17152  cvgcmp2n  17204  iswomninnlem  17221  nconstwlpo  17238