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

Theorem adantllr 718
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 457 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 650 1  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  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:  adantl3r  749  r19.29an  2995  oewordri  7231  marypha1lem  7882  gruwun  9180  lemul12b  10388  rlimsqzlem  13420  fsumrlim  13574  fsumo1  13575  isacs2  14897  tgcl  19230  neindisj  19377  neiptoptop  19391  isr0  19966  cnextcn  20295  ustuqtop4  20475  utopsnneiplem  20478  metss  20739  restmetu  20818  mbfsup  21799  itg2i1fseqle  21889  ditgsplit  21993  itgulm  22530  leibpi  22994  dchrisumlem3  23397  legov  23692  legov2  23693  legtrid  23698  colline  23736  f1otrg  23843  cusgrasize2inds  24139  grpoidinvlem3  24734  grpoideu  24737  grporcan  24749  isgrp2d  24763  blocni  25246  normcan  26020  unoplin  26365  hmoplin  26387  nmophmi  26476  mdslmd3i  26777  chirredlem1  26835  chirredlem2  26836  mdsymlem5  26852  cdj1i  26878  isarchi3  27243  archiabllem1  27249  archiabl  27254  isarchiofld  27320  pstmxmet  27362  ordtconlem1  27392  esumcvg  27582  eulerpartlemgvv  27805  signstfvneq0  28019  heicant  29477  itg2addnclem  29494  ftc1anclem5  29522  ftc1anclem6  29523  ftc1anclem7  29524  ftc1anclem8  29525  ftc1anc  29526  elicc3  29563  fzmul  29687  fdc  29692  fdc1  29693  incsequz2  29696  rrncmslem  29782  ghomco  29799  rngoisocnv  29838  ispridlc  29921  ssfiunibd  30905  islpcn  31000  lptre2pt  31001  0ellimcdiv  31010  limclner  31012  icccncfext  31045  cncfiooiccre  31053  fperdvper  31067  itgioocnicc  31114  stoweidlem35  31154  wallispilem3  31186  fourierdlem20  31246  fourierdlem34  31260  fourierdlem39  31265  fourierdlem42  31268  fourierdlem46  31272  fourierdlem48  31274  fourierdlem49  31275  fourierdlem50  31276  fourierdlem63  31289  fourierdlem64  31290  fourierdlem73  31299  fourierdlem77  31303  fourierdlem81  31307  fourierdlem87  31313  fourierdlem97  31323  fourierdlem103  31329  fourierdlem104  31330  fourierdlem111  31337
  Copyright terms: Public domain W3C validator