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

Theorem rexlimd 2941
Description: Deduction form of rexlimd 2941. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)
Hypotheses
Ref Expression
rexlimd.1
rexlimd.2
rexlimd.3
Assertion
Ref Expression
rexlimd

Proof of Theorem rexlimd
StepHypRef Expression
1 rexlimd.1 . 2
2 rexlimd.2 . . 3
32a1i 11 . 2
4 rexlimd.3 . 2
51, 3, 4rexlimd2 2940 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  F/wnf 1616  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rexlimdvOLD  2948  r19.29af2  2995  reusv2lem2  4654  reusv6OLD  4663  ralxfrALT  4671  fvmptt  5971  ffnfv  6057  peano5  6723  tz7.49  7129  nneneq  7720  ac6sfi  7784  ixpiunwdom  8038  r1val1  8225  rankuni2b  8292  infpssrlem4  8707  zorn2lem4  8900  zorn2lem5  8901  konigthlem  8964  tskuni  9182  gruiin  9209  lbzbi  11199  iunconlem  19928  ptbasfi  20082  alexsubALTlem3  20549  ovoliunnul  21918  iunmbl2  21967  mptelee  24198  atom1d  27272  elabreximd  27408  iundisjf  27448  esumc  28062  heicant  30049  indexa  30224  sdclem2  30235  refsumcn  31405  suprnmpt  31451  upbdrech  31505  ssfiunibd  31509  iccshift  31558  iooshift  31562  fmul01lt1  31580  fprodle  31604  islptre  31625  rexlim2d  31631  limcperiod  31634  islpcn  31645  limclner  31657  dvnprodlem1  31743  dvnprodlem2  31744  itgperiod  31780  stoweidlem29  31811  stoweidlem31  31813  stoweidlem59  31841  stirlinglem13  31868  fourierdlem48  31937  fourierdlem51  31940  fourierdlem53  31942  fourierdlem80  31969  fourierdlem81  31970  fourierdlem93  31982  elaa2  32017  ffnafv  32256  2zrngagrp  32749  glbconxN  35102  cdleme26ee  36086  cdleme32d  36170  cdleme32f  36172  cdlemk38  36641  cdlemk19x  36669  cdlemk11t  36672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator