Theorem adantlll 729

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 467	. 2 |- ( ( ta /\ ph ) -> ph )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl1 660	1 |- ( ( ( ( ta /\ ph ) /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  fun11iun  6779  oewordri  7318  sbthlem8  7714  xmulass  11601  caucvgb  13794  clsnsg  21172  metustto  21616  constr3cycl  25437  grpoidinvlem3  25982  nmoub3i  26462  riesz3i  27763  csmdsymi  28035  finxpreclem3  31829  fin2so  31976  mblfinlem2  32022  mblfinlem3  32023  ismblfin  32025  itg2addnclem  32037  ftc1anclem7  32067  ftc1anc  32069  fzmul  32113  fdc  32118  incsequz2  32122  isbnd3  32160  bndss  32162  ismtyres  32184  rngoisocnv  32264  xralrple2  37614  dirkertrigeq  38000  fourierdlem12  38018  fourierdlem50  38057  fourierdlem103  38110  fourierdlem104  38111  etransclem35  38171  sge0iunmptlemfi  38292  iundjiun  38335  hoidmvle  38459  ovnhoilem2  38461