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  6408  oelim  6549  odi  6593  marypha1lem  7202  dfac12lem2  7786  infunsdom  7856  isf34lem4  8019  distrlem1pr  8665  drsdirfi  14088  isacs3lem  14285  conjnmzb  14733  metss2lem  18073  nghmcn  18270  bndth  18472  itg2monolem1  19121  dvmptfsum  19338  ply1divex  19538  itgulm  19800  rpvmasumlem  20652  dchrmusum2  20659  dchrisum0lem2  20683  dchrisum0lem3  20684  mulog2sumlem2  20700  pntibndlem3  20757  blocni  21399  superpos  22950  chirredlem2  22987  ballotlemfc0  23067  ballotlemfcc  23068  itg2addnclem  25003  fdc  26558  incsequz  26561  ismtyres  26635  isdrngo2  26692  rngohomco  26708  keridl  26760  mzpcompact2lem  26932  pellex  27023  monotuz  27129  frlmsslsp  27351  3v3e3cycl1  28390  4cycl4v4e  28412  linepsubN  30563  pmapsub  30579
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