MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantlrr Structured version   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  6637  oelim  6778  odi  6822  marypha1lem  7438  dfac12lem2  8024  infunsdom  8094  isf34lem4  8257  distrlem1pr  8902  drsdirfi  14395  isacs3lem  14592  conjnmzb  15040  metss2lem  18541  nghmcn  18779  bndth  18983  itg2monolem1  19642  dvmptfsum  19859  ply1divex  20059  itgulm  20324  rpvmasumlem  21181  dchrmusum2  21188  dchrisum0lem2  21212  dchrisum0lem3  21213  mulog2sumlem2  21229  pntibndlem3  21286  3v3e3cycl1  21631  4cycl4v4e  21653  blocni  22306  superpos  23857  chirredlem2  23894  ballotlemfc0  24750  ballotlemfcc  24751  ftc1anclem6  26285  ftc1anc  26288  fdc  26449  incsequz  26452  ismtyres  26517  isdrngo2  26574  rngohomco  26590  keridl  26642  mzpcompact2lem  26808  pellex  26898  monotuz  27004  frlmsslsp  27225  stoweidlem34  27759  linepsubN  30549  pmapsub  30565
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