Theorem adantlrr 720

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
adantlrr

Proof of Theorem adantlrr

Step	Hyp	Ref	Expression
1		simpl 457	. 2
2		adantl2.1	. 2
3	1, 2	sylanl2 651	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  oelim  7203  odi  7247  marypha1lem  7913  dfac12lem2  8545  infunsdom  8615  isf34lem4  8778  distrlem1pr  9424  drsdirfi  15567  isacs3lem  15796  conjnmzb  16301  psgndif  18638  frlmsslsp  18829  frlmsslspOLD  18830  metss2lem  21014  nghmcn  21252  bndth  21458  itg2monolem1  22157  dvmptfsum  22376  ply1divex  22537  itgulm  22803  rpvmasumlem  23672  dchrmusum2  23679  dchrisum0lem2  23703  dchrisum0lem3  23704  mulog2sumlem2  23720  pntibndlem3  23777  3v3e3cycl1  24644  4cycl4v4e  24666  blocni  25720  superpos  27273  chirredlem2  27310  eulerpartlemgvv  28315  ballotlemfc0  28431  ballotlemfcc  28432  fin2solem  30039  heicant  30049  ftc1anclem6  30095  ftc1anc  30098  fdc  30238  incsequz  30241  ismtyres  30304  isdrngo2  30361  rngohomco  30377  keridl  30429  mzpcompact2lem  30684  pellex  30771  monotuz  30877  unxpwdom3  31041  radcnvrat  31195  lcmgcdlem  31212  lcmdvds  31214  fprodexp  31600  fprodabs2  31602  dvnprodlem1  31743  stoweidlem34  31816  fourierdlem42  31931  elaa2  32017  aacllem  33216  bj-finsumval0  34663  linepsubN  35476  pmapsub  35492

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