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  2982  oewordri  7239  marypha1lem  7891  gruwun  9189  lemul12b  10400  rlimsqzlem  13445  fsumrlim  13599  fsumo1  13600  isacs2  14922  tgcl  19337  neindisj  19484  neiptoptop  19498  isr0  20104  cnextcn  20433  ustuqtop4  20613  metss  20877  mbfsup  21937  itg2i1fseqle  22027  ditgsplit  22131  itgulm  22668  leibpi  23138  dchrisumlem3  23541  legov  23837  legov2  23838  legtrid  23843  f1otrg  24039  cusgrasize2inds  24342  grpoidinvlem3  25073  grpoideu  25076  grporcan  25088  isgrp2d  25102  blocni  25585  normcan  26359  unoplin  26704  hmoplin  26726  nmophmi  26815  mdslmd3i  27116  chirredlem1  27174  chirredlem2  27175  mdsymlem5  27191  cdj1i  27217  fpwrelmap  27421  archiabllem1  27603  archiabl  27608  isarchiofld  27673  locfinreflem  27709  pstmxmet  27742  ordtconlem1  27772  esumcvg  27958  signstfvneq0  28395  heicant  30017  itg2addnclem  30034  ftc1anclem5  30062  ftc1anclem6  30063  ftc1anclem7  30064  ftc1anclem8  30065  ftc1anc  30066  elicc3  30103  fzmul  30201  fdc  30206  fdc1  30207  incsequz2  30210  rrncmslem  30296  ghomco  30313  rngoisocnv  30352  ispridlc  30435  cvgdvgrat  31163  lcmdvds  31183  lptre2pt  31550  0ellimcdiv  31559  limclner  31561  icccncfext  31593  cncfiooiccre  31601  fperdvper  31615  iblcncfioo  31663  stoweidlem35  31702  wallispilem3  31734  fourierdlem20  31794  fourierdlem34  31808  fourierdlem39  31813  fourierdlem42  31816  fourierdlem46  31820  fourierdlem48  31822  fourierdlem49  31823  fourierdlem63  31837  fourierdlem64  31838  fourierdlem73  31847  fourierdlem87  31861  fourierdlem97  31871  fourierdlem103  31877  fourierdlem104  31878  fourierdlem111  31885
  Copyright terms: Public domain W3C validator