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  6392  oelim  6533  odi  6577  marypha1lem  7186  dfac12lem2  7770  infunsdom  7840  isf34lem4  8003  distrlem1pr  8649  drsdirfi  14072  isacs3lem  14269  conjnmzb  14717  metss2lem  18057  nghmcn  18254  bndth  18456  itg2monolem1  19105  dvmptfsum  19322  ply1divex  19522  itgulm  19784  rpvmasumlem  20636  dchrmusum2  20643  dchrisum0lem2  20667  dchrisum0lem3  20668  mulog2sumlem2  20684  pntibndlem3  20741  blocni  21383  superpos  22934  chirredlem2  22971  ballotlemfc0  23051  ballotlemfcc  23052  fdc  26455  incsequz  26458  ismtyres  26532  isdrngo2  26589  rngohomco  26605  keridl  26657  mzpcompact2lem  26829  pellex  26920  monotuz  27026  frlmsslsp  27248  linepsubN  29941  pmapsub  29957
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