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  7023  marypha1lem  7675  gruwun  8972  lemul12b  10178  rlimsqzlem  13118  fsumrlim  13266  fsumo1  13267  isacs2  14583  tgcl  18554  neindisj  18701  neiptoptop  18715  isr0  19290  cnextcn  19619  ustuqtop4  19799  utopsnneiplem  19802  metss  20063  restmetu  20142  mbfsup  21122  itg2i1fseqle  21212  ditgsplit  21316  itgulm  21853  leibpi  22317  dchrisumlem3  22720  legov  22996  legov2  22997  legtrid  23002  colline  23032  f1otrg  23085  cusgrasize2inds  23353  grpoidinvlem3  23661  grpoideu  23664  grporcan  23676  isgrp2d  23690  blocni  24173  normcan  24947  unoplin  25292  hmoplin  25314  nmophmi  25403  mdslmd3i  25704  chirredlem1  25762  chirredlem2  25763  mdsymlem5  25779  cdj1i  25805  isarchi3  26172  archiabllem1  26178  archiabl  26183  isarchiofld  26253  pstmxmet  26293  ordtconlem1  26323  esumcvg  26504  eulerpartlemgvv  26728  signstfvneq0  26942  heicant  28397  itg2addnclem  28414  ftc1anclem5  28442  ftc1anclem6  28443  ftc1anclem7  28444  ftc1anclem8  28445  ftc1anc  28446  elicc3  28483  fzmul  28607  fdc  28612  fdc1  28613  incsequz2  28616  rrncmslem  28702  ghomco  28719  rngoisocnv  28758  ispridlc  28841  stoweidlem35  29801  wallispilem3  29833
  Copyright terms: Public domain W3C validator