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

Theorem adantllr 711
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 454 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 643 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  742  oewordri  7019  marypha1lem  7671  gruwun  8968  lemul12b  10174  rlimsqzlem  13110  fsumrlim  13257  fsumo1  13258  isacs2  14574  tgcl  18416  neindisj  18563  neiptoptop  18577  isr0  19152  cnextcn  19481  ustuqtop4  19661  utopsnneiplem  19664  metss  19925  restmetu  20004  mbfsup  20984  itg2i1fseqle  21074  ditgsplit  21178  itgulm  21758  leibpi  22222  dchrisumlem3  22625  legov  22892  legov2  22893  legtrid  22898  colline  22918  f1otrg  22940  cusgrasize2inds  23208  grpoidinvlem3  23516  grpoideu  23519  grporcan  23531  isgrp2d  23545  blocni  24028  normcan  24802  unoplin  25147  hmoplin  25169  nmophmi  25258  mdslmd3i  25559  chirredlem1  25617  chirredlem2  25618  mdsymlem5  25634  cdj1i  25660  isarchi3  26028  archiabllem1  26034  archiabl  26039  isarchiofld  26138  pstmxmet  26178  ordtconlem1  26208  esumcvg  26389  eulerpartlemgvv  26607  signstfvneq0  26821  heicant  28270  itg2addnclem  28287  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  elicc3  28356  fzmul  28480  fdc  28485  fdc1  28486  incsequz2  28489  rrncmslem  28575  ghomco  28592  rngoisocnv  28631  ispridlc  28714  stoweidlem35  29676  wallispilem3  29708
  Copyright terms: Public domain W3C validator