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

Theorem adantlrr 701
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 443 . 2  |-  ( ( ps  /\  ta )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 632 1  |-  ( ( ( ph  /\  ( ps  /\  ta ) )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  tfrlem2  6534  oelim  6675  odi  6719  marypha1lem  7333  dfac12lem2  7917  infunsdom  7987  isf34lem4  8150  distrlem1pr  8796  drsdirfi  14282  isacs3lem  14479  conjnmzb  14927  metss2lem  18270  nghmcn  18467  bndth  18671  itg2monolem1  19320  dvmptfsum  19537  ply1divex  19737  itgulm  20002  rpvmasumlem  20859  dchrmusum2  20866  dchrisum0lem2  20890  dchrisum0lem3  20891  mulog2sumlem2  20907  pntibndlem3  20964  blocni  21696  superpos  23247  chirredlem2  23284  ballotlemfc0  24198  ballotlemfcc  24199  itg2addnclem  25675  fdc  25962  incsequz  25965  ismtyres  26038  isdrngo2  26095  rngohomco  26111  keridl  26163  mzpcompact2lem  26335  pellex  26426  monotuz  26532  frlmsslsp  26754  3v3e3cycl1  27770  4cycl4v4e  27792  linepsubN  30012  pmapsub  30028
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