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  6364  oewordri  6606  marypha1lem  7202  gruwun  8451  lemul12b  9629  rlimsqzlem  12138  fsumrlim  12285  fsumo1  12286  isacs2  13571  tgcl  16723  neindisj  16870  isr0  17444  metss  18070  mbfsup  19035  itg2i1fseqle  19125  ditgsplit  19227  itgulm  19800  leibpi  20254  dchrisumlem3  20656  grpoidinvlem3  20889  grpoideu  20892  grporcan  20904  isgrp2d  20918  blocni  21399  normcan  22171  unoplin  22516  hmoplin  22538  nmophmi  22627  mdslmd3i  22928  chirredlem1  22986  chirredlem2  22987  mdsymlem5  23003  cdj1i  23029  esumcvg  23469  itg2addnclem  25003  elicc3  26331  fzmul  26546  fdc  26558  fdc1  26559  incsequz2  26562  rrncmslem  26659  ghomco  26676  rngoisocnv  26715  ispridlc  26798  unxpwdom3  27359
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