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

Theorem adantlll 698
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 447 . 2  |-  ( ( ta  /\  ph )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 631 1  |-  ( ( ( ( ta  /\  ph )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fun11iun  5509  oewordri  6606  sbthlem8  6994  xmulass  10623  caucvgb  12168  clsnsg  17808  grpoidinvlem3  20889  nmoub3i  21367  riesz3i  22658  csmdsymi  22930  itg2addnclem  25003  itg2addnc  25005  fzmul  26546  fdc  26558  incsequz2  26562  isbnd3  26611  bndss  26613  ismtyres  26635  rngoisocnv  26715  constr3cycl  28407
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 177  df-an 360
  Copyright terms: Public domain W3C validator