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  oewordri  7131  marypha1lem  7784  gruwun  9081  lemul12b  10287  rlimsqzlem  13228  fsumrlim  13376  fsumo1  13377  isacs2  14693  tgcl  18690  neindisj  18837  neiptoptop  18851  isr0  19426  cnextcn  19755  ustuqtop4  19935  utopsnneiplem  19938  metss  20199  restmetu  20278  mbfsup  21258  itg2i1fseqle  21348  ditgsplit  21452  itgulm  21989  leibpi  22453  dchrisumlem3  22856  legov  23137  legov2  23138  legtrid  23143  colline  23177  f1otrg  23252  cusgrasize2inds  23520  grpoidinvlem3  23828  grpoideu  23831  grporcan  23843  isgrp2d  23857  blocni  24340  normcan  25114  unoplin  25459  hmoplin  25481  nmophmi  25570  mdslmd3i  25871  chirredlem1  25929  chirredlem2  25930  mdsymlem5  25946  cdj1i  25972  isarchi3  26338  archiabllem1  26344  archiabl  26349  isarchiofld  26419  pstmxmet  26458  ordtconlem1  26488  esumcvg  26669  eulerpartlemgvv  26893  signstfvneq0  27107  heicant  28564  itg2addnclem  28581  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  elicc3  28650  fzmul  28774  fdc  28779  fdc1  28780  incsequz2  28783  rrncmslem  28869  ghomco  28886  rngoisocnv  28925  ispridlc  29008  stoweidlem35  29968  wallispilem3  30000
  Copyright terms: Public domain W3C validator