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

Theorem adantllr 699
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
adantllr  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )

Proof of Theorem adantllr
StepHypRef Expression
1 simpl 443 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 631 1  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  riotasvdOLD  6348  oewordri  6590  marypha1lem  7186  gruwun  8435  lemul12b  9613  rlimsqzlem  12122  fsumrlim  12269  fsumo1  12270  isacs2  13555  tgcl  16707  neindisj  16854  isr0  17428  metss  18054  mbfsup  19019  itg2i1fseqle  19109  ditgsplit  19211  itgulm  19784  leibpi  20238  dchrisumlem3  20640  grpoidinvlem3  20873  grpoideu  20876  grporcan  20888  isgrp2d  20902  blocni  21383  normcan  22155  unoplin  22500  hmoplin  22522  nmophmi  22611  mdslmd3i  22912  chirredlem1  22970  chirredlem2  22971  mdsymlem5  22987  cdj1i  23013  esumcvg  23454  elicc3  26228  fzmul  26443  fdc  26455  fdc1  26456  incsequz2  26459  rrncmslem  26556  ghomco  26573  rngoisocnv  26612  ispridlc  26695  unxpwdom3  27256
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