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  6734  oewordri  7231  sbthlem8  7624  xmulass  11468  caucvgb  13451  clsnsg  20336  metusttoOLD  20788  metustto  20789  constr3cycl  24323  grpoidinvlem3  24870  nmoub3i  25350  riesz3i  26643  csmdsymi  26915  fin2so  29603  heicant  29613  mblfinlem2  29616  mblfinlem3  29617  ismblfin  29619  itg2addnclem  29630  ftc1anclem7  29660  ftc1anc  29662  fzmul  29823  fdc  29828  incsequz2  29832  isbnd3  29870  bndss  29872  ismtyres  29894  rngoisocnv  29974  dirkertrigeq  31356  fourierdlem12  31374  fourierdlem50  31412  fourierdlem103  31465  fourierdlem104  31466
  Copyright terms: Public domain W3C validator