Theorem adantlll 717

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

Hypothesis

Ref	Expression
adantl2.1

Assertion

Ref	Expression
adantlll

Proof of Theorem adantlll

Step	Hyp	Ref	Expression
1		simpr 461	. 2
2		adantl2.1	. 2
3	1, 2	sylanl1 650	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  fun11iun  6760  oewordri  7260  sbthlem8  7654  xmulass  11508  caucvgb  13502  clsnsg  20608  metusttoOLD  21060  metustto  21061  constr3cycl  24661  grpoidinvlem3  25208  nmoub3i  25688  riesz3i  26981  csmdsymi  27253  fin2so  30040  heicant  30049  mblfinlem2  30052  mblfinlem3  30053  ismblfin  30055  itg2addnclem  30066  ftc1anclem7  30096  ftc1anc  30098  fzmul  30233  fdc  30238  incsequz2  30242  isbnd3  30280  bndss  30282  ismtyres  30304  rngoisocnv  30384  dirkertrigeq  31883  fourierdlem12  31901  fourierdlem50  31939  fourierdlem103  31992  fourierdlem104  31993  etransclem35  32052

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