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	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
adantlll	|- ( ( ( ( ta /\ ph ) /\ ps ) /\ ch ) -> th )

Proof of Theorem adantlll

Step	Hyp	Ref	Expression
1		simpr 461	. 2 |- ( ( ta /\ ph ) -> ph )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl1 650	1 |- ( ( ( ( ta /\ ph ) /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

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

This theorem is referenced by:  fun11iun  6734  oewordri  7231  sbthlem8  7624  xmulass  11468  caucvgb  13451  clsnsg  20336  metusttoOLD  20788  metustto  20789  constr3cycl  24323  grpoidinvlem3  24870  nmoub3i  25350  riesz3i  26643  csmdsymi  26915  fin2so  29603  heicant  29613  mblfinlem2  29616  mblfinlem3  29617  ismblfin  29619  itg2addnclem  29630  ftc1anclem7  29660  ftc1anc  29662  fzmul  29823  fdc  29828  incsequz2  29832  isbnd3  29870  bndss  29872  ismtyres  29894  rngoisocnv  29974  dirkertrigeq  31356  fourierdlem12  31374  fourierdlem50  31412  fourierdlem103  31465  fourierdlem104  31466