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

Theorem adantlrr 715
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 454 . 2  |-  ( ( ps  /\  ta )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 646 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  6970  odi  7014  marypha1lem  7679  dfac12lem2  8309  infunsdom  8379  isf34lem4  8542  distrlem1pr  9190  drsdirfi  15104  isacs3lem  15332  conjnmzb  15774  psgndif  17991  frlmsslsp  18182  frlmsslspOLD  18183  metss2lem  20045  nghmcn  20283  bndth  20489  itg2monolem1  21187  dvmptfsum  21406  ply1divex  21567  itgulm  21832  rpvmasumlem  22695  dchrmusum2  22702  dchrisum0lem2  22726  dchrisum0lem3  22727  mulog2sumlem2  22743  pntibndlem3  22800  3v3e3cycl1  23465  4cycl4v4e  23487  blocni  24140  superpos  25693  chirredlem2  25730  eulerpartlemgvv  26689  ballotlemfc0  26805  ballotlemfcc  26806  fin2solem  28340  heicant  28351  ftc1anclem6  28397  ftc1anc  28400  fdc  28566  incsequz  28569  ismtyres  28632  isdrngo2  28689  rngohomco  28705  keridl  28757  mzpcompact2lem  29013  pellex  29101  monotuz  29207  unxpwdom3  29373  stoweidlem34  29754  bj-finsumval0  32308  linepsubN  33118  pmapsub  33134
  Copyright terms: Public domain W3C validator