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

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