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  2998  oewordri  7259  marypha1lem  7911  gruwun  9208  lemul12b  10420  rlimsqzlem  13483  fsumrlim  13637  fsumo1  13638  isacs2  15070  tgcl  19598  neindisj  19745  neiptoptop  19759  isr0  20364  cnextcn  20693  ustuqtop4  20873  metss  21137  mbfsup  22197  itg2i1fseqle  22287  ditgsplit  22391  itgulm  22929  leibpi  23399  dchrisumlem3  23802  legov  24098  legov2  24099  legtrid  24104  f1otrg  24301  cusgrasize2inds  24604  grpoidinvlem3  25335  grpoideu  25338  grporcan  25350  isgrp2d  25364  blocni  25847  normcan  26621  unoplin  26966  hmoplin  26988  nmophmi  27077  mdslmd3i  27378  chirredlem1  27436  chirredlem2  27437  mdsymlem5  27453  cdj1i  27479  elsnxp  27612  fpwrelmap  27713  archiabllem1  27897  archiabl  27902  isarchiofld  27968  locfinreflem  28004  pstmxmet  28037  ordtconlem1  28067  esumcvg  28258  esum2d  28265  esumiun  28266  omssubadd  28444  signstfvneq0  28726  heicant  30254  itg2addnclem  30271  ftc1anclem5  30299  ftc1anclem6  30300  ftc1anclem7  30301  ftc1anclem8  30302  ftc1anc  30303  elicc3  30340  fzmul  30438  fdc  30443  fdc1  30444  incsequz2  30447  rrncmslem  30533  ghomco  30550  rngoisocnv  30589  ispridlc  30672  cvgdvgrat  31398  lcmdvds  31418  binomcxplemnotnn0  31465  lptre2pt  31849  0ellimcdiv  31858  limclner  31860  icccncfext  31893  cncfiooiccre  31901  fperdvper  31918  dvnprodlem2  31947  iblcncfioo  31980  stoweidlem35  32020  wallispilem3  32052  fourierdlem20  32112  fourierdlem34  32126  fourierdlem39  32131  fourierdlem42  32134  fourierdlem46  32138  fourierdlem48  32140  fourierdlem49  32141  fourierdlem63  32155  fourierdlem64  32156  fourierdlem73  32165  fourierdlem87  32179  fourierdlem97  32189  fourierdlem103  32195  fourierdlem104  32196  fourierdlem111  32203  etransclem32  32252  etransclem33  32253  etransclem35  32255  aacllem  33360
  Copyright terms: Public domain W3C validator