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

Theorem adantlrr 702
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
adantlrr  |-  ( ( ( ph  /\  ( ps  /\  ta ) )  /\  ch )  ->  th )

Proof of Theorem adantlrr
StepHypRef Expression
1 simpl 444 . 2  |-  ( ( ps  /\  ta )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 633 1  |-  ( ( ( ph  /\  ( ps  /\  ta ) )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  tfrlem2  6596  oelim  6737  odi  6781  marypha1lem  7396  dfac12lem2  7980  infunsdom  8050  isf34lem4  8213  distrlem1pr  8858  drsdirfi  14350  isacs3lem  14547  conjnmzb  14995  metss2lem  18494  nghmcn  18732  bndth  18936  itg2monolem1  19595  dvmptfsum  19812  ply1divex  20012  itgulm  20277  rpvmasumlem  21134  dchrmusum2  21141  dchrisum0lem2  21165  dchrisum0lem3  21166  mulog2sumlem2  21182  pntibndlem3  21239  3v3e3cycl1  21584  4cycl4v4e  21606  blocni  22259  superpos  23810  chirredlem2  23847  ballotlemfc0  24703  ballotlemfcc  24704  fdc  26339  incsequz  26342  ismtyres  26407  isdrngo2  26464  rngohomco  26480  keridl  26532  mzpcompact2lem  26698  pellex  26788  monotuz  26894  frlmsslsp  27116  stoweidlem34  27650  linepsubN  30234  pmapsub  30250
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 178  df-an 361
  Copyright terms: Public domain W3C validator