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

Theorem adantlrr 720
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 457 . 2  |-  ( ( ps  /\  ta )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 651 1  |-  ( ( ( ph  /\  ( ps  /\  ta ) )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  oelim  7181  odi  7225  marypha1lem  7889  dfac12lem2  8520  infunsdom  8590  isf34lem4  8753  distrlem1pr  9399  drsdirfi  15421  isacs3lem  15649  conjnmzb  16096  psgndif  18405  frlmsslsp  18596  frlmsslspOLD  18597  metss2lem  20749  nghmcn  20987  bndth  21193  itg2monolem1  21892  dvmptfsum  22111  ply1divex  22272  itgulm  22537  rpvmasumlem  23400  dchrmusum2  23407  dchrisum0lem2  23431  dchrisum0lem3  23432  mulog2sumlem2  23448  pntibndlem3  23505  3v3e3cycl1  24320  4cycl4v4e  24342  blocni  25396  superpos  26949  chirredlem2  26986  eulerpartlemgvv  27955  ballotlemfc0  28071  ballotlemfcc  28072  fin2solem  29616  heicant  29626  ftc1anclem6  29672  ftc1anc  29675  fdc  29841  incsequz  29844  ismtyres  29907  isdrngo2  29964  rngohomco  29980  keridl  30032  mzpcompact2lem  30288  pellex  30375  monotuz  30481  unxpwdom3  30645  lcmgcdlem  30812  lcmdvds  30814  stoweidlem34  31334  fourierdlem42  31449  bj-finsumval0  33735  linepsubN  34548  pmapsub  34564
  Copyright terms: Public domain W3C validator