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

Theorem adantllr 700
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 444 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 632 1  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  riotasvdOLD  6593  oewordri  6835  marypha1lem  7438  gruwun  8688  lemul12b  9867  rlimsqzlem  12442  fsumrlim  12590  fsumo1  12591  isacs2  13878  tgcl  17034  neindisj  17181  neiptoptop  17195  isr0  17769  cnextcn  18098  ustuqtop4  18274  utopsnneiplem  18277  metss  18538  restmetu  18617  mbfsup  19556  itg2i1fseqle  19646  ditgsplit  19748  itgulm  20324  leibpi  20782  dchrisumlem3  21185  cusgrasize2inds  21486  grpoidinvlem3  21794  grpoideu  21797  grporcan  21809  isgrp2d  21823  blocni  22306  normcan  23078  unoplin  23423  hmoplin  23445  nmophmi  23534  mdslmd3i  23835  chirredlem1  23893  chirredlem2  23894  mdsymlem5  23910  cdj1i  23936  adantl3r  23956  pstmxmet  24292  esumcvg  24476  itg2addnclem  26256  ftc1anclem5  26284  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  elicc3  26320  fzmul  26444  fdc  26449  fdc1  26450  incsequz2  26453  rrncmslem  26541  ghomco  26558  rngoisocnv  26597  ispridlc  26680  unxpwdom3  27233  stoweidlem35  27760  wallispilem3  27792  cshwsame  28277
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 178  df-an 361
  Copyright terms: Public domain W3C validator