Theorem adantllr 718

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1

Assertion

Ref	Expression
adantllr

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		simpl 457	. 2
2		adantl2.1	. 2
3	1, 2	sylanl1 650	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  adantl3r  749  r19.29an  2998  oewordri  7260  marypha1lem  7913  gruwun  9212  lemul12b  10424  rlimsqzlem  13471  fsumrlim  13625  fsumo1  13626  isacs2  15050  tgcl  19471  neindisj  19618  neiptoptop  19632  isr0  20238  cnextcn  20567  ustuqtop4  20747  metss  21011  mbfsup  22071  itg2i1fseqle  22161  ditgsplit  22265  itgulm  22803  leibpi  23273  dchrisumlem3  23676  legov  23972  legov2  23973  legtrid  23978  f1otrg  24174  cusgrasize2inds  24477  grpoidinvlem3  25208  grpoideu  25211  grporcan  25223  isgrp2d  25237  blocni  25720  normcan  26494  unoplin  26839  hmoplin  26861  nmophmi  26950  mdslmd3i  27251  chirredlem1  27309  chirredlem2  27310  mdsymlem5  27326  cdj1i  27352  fpwrelmap  27556  archiabllem1  27737  archiabl  27742  isarchiofld  27807  locfinreflem  27843  pstmxmet  27876  ordtconlem1  27906  esumcvg  28092  signstfvneq0  28529  heicant  30049  itg2addnclem  30066  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  elicc3  30135  fzmul  30233  fdc  30238  fdc1  30239  incsequz2  30242  rrncmslem  30328  ghomco  30345  rngoisocnv  30384  ispridlc  30467  cvgdvgrat  31194  lcmdvds  31214  binomcxplemnotnn0  31261  lptre2pt  31646  0ellimcdiv  31655  limclner  31657  icccncfext  31690  cncfiooiccre  31698  fperdvper  31715  dvnprodlem2  31744  iblcncfioo  31777  stoweidlem35  31817  wallispilem3  31849  fourierdlem20  31909  fourierdlem34  31923  fourierdlem39  31928  fourierdlem42  31931  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem63  31952  fourierdlem64  31953  fourierdlem73  31962  fourierdlem87  31976  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  etransclem32  32049  etransclem33  32050  etransclem35  32052  aacllem  33216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371