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

Theorem adantlll 715
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 459 . 2  |-  ( ( ta  /\  ph )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 648 1  |-  ( ( ( ( ta  /\  ph )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  fun11iun  6733  oewordri  7233  sbthlem8  7627  xmulass  11482  caucvgb  13587  clsnsg  20777  metusttoOLD  21229  metustto  21230  constr3cycl  24866  grpoidinvlem3  25409  nmoub3i  25889  riesz3i  27182  csmdsymi  27454  fin2so  30283  heicant  30292  mblfinlem2  30295  mblfinlem3  30296  ismblfin  30298  itg2addnclem  30309  ftc1anclem7  30339  ftc1anc  30341  fzmul  30476  fdc  30481  incsequz2  30485  isbnd3  30523  bndss  30525  ismtyres  30547  rngoisocnv  30627  dirkertrigeq  32125  fourierdlem12  32143  fourierdlem50  32181  fourierdlem103  32234  fourierdlem104  32235  etransclem35  32294
  Copyright terms: Public domain W3C validator