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  6537  oewordri  7031  sbthlem8  7428  xmulass  11250  caucvgb  13157  clsnsg  19680  metusttoOLD  20132  metustto  20133  constr3cycl  23547  grpoidinvlem3  23693  nmoub3i  24173  riesz3i  25466  csmdsymi  25738  fin2so  28416  heicant  28426  mblfinlem2  28429  mblfinlem3  28430  ismblfin  28432  itg2addnclem  28443  ftc1anclem7  28473  ftc1anc  28475  fzmul  28636  fdc  28641  incsequz2  28645  isbnd3  28683  bndss  28685  ismtyres  28707  rngoisocnv  28787