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

Theorem adantlll 700
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 449 . 2  |-  ( ( ta  /\  ph )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 633 1  |-  ( ( ( ( ta  /\  ph )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  fun11iun  5697  oewordri  6837  sbthlem8  7226  xmulass  10868  caucvgb  12475  clsnsg  18141  metusttoOLD  18589  metustto  18590  constr3cycl  21650  grpoidinvlem3  21796  nmoub3i  22276  riesz3i  23567  csmdsymi  23839  mblfinlem2  26246  mblfinlem3  26247  ismblfin  26249  itg2addnclem  26258  ftc1anclem7  26288  ftc1anc  26290  fzmul  26446  fdc  26451  incsequz2  26455  isbnd3  26495  bndss  26497  ismtyres  26519  rngoisocnv  26599
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator