Theorem exlimi 1912

Description: Inference associated with 19.23 1910. See exlimiv 1722 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
exlimi.1
exlimi.2

Assertion

Ref	Expression
exlimi

Proof of Theorem exlimi

Step	Hyp	Ref	Expression
1		exlimi.1	. . 3
2	1	19.23 1910	. 2
3		exlimi.2	. 2
4	2, 3	mpgbi 1621	1

Syntax hints:  ->wi 4  E.wex 1612  F/wnf 1616

This theorem is referenced by:  exlimih  1913  equs5a  1978  equs5e  1979  equsex  2038  nfeqf2  2041  exdistrf  2075  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  moanim  2350  euan  2351  moexex  2363  2eu6  2383  ceqsex  3145  sbhypf  3156  vtoclgf  3165  vtoclg1f  3166  vtoclef  3182  rspn0  3797  reusv2lem1  4653  copsexg  4737  copsexgOLD  4738  copsex2g  4740  ralxpf  5154  dmcoss  5267  fv3  5884  tz6.12c  5890  opabiota  5936  0neqopab  6341  zfregcl  8041  scottex  8324  scott0  8325  dfac5lem5  8529  zfcndpow  9015  zfcndreg  9016  zfcndinf  9017  reclem2pr  9447  uzindOLD  10982  mreiincl  14993  cnvoprab  27546  exisym1  29889  eu2ndop1stv  32207  bnj607  33974  bnj900  33987  bj-equsexv  34312  exlimii  34404  bj-exlimmpi  34477  bj-exlimmpbi  34478  bj-exlimmpbir  34479  dihglblem5  37025

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-ex 1613  df-nf 1617