MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantlll Structured version   Unicode version

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
StepHypRef Expression
1 simpr 461 . 2  |-  ( ( ta  /\  ph )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 650 1  |-  ( ( ( ( ta  /\  ph )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator