Theorem 2eximdv 1712

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1654. (Contributed by NM, 3-Aug-1995.)

Hypothesis

Ref	Expression
2alimdv.1

Assertion

Ref	Expression
2eximdv

Distinct variable groups:   ,   ,

Proof of Theorem 2eximdv

Step	Hyp	Ref	Expression
1		2alimdv.1	. . 3
2	1	eximdv 1710	. 2
3	2	eximdv 1710	1

Syntax hints:  ->wi 4  E.wex 1612

This theorem is referenced by:  2eu6  2383  cgsex2g  3143  cgsex4g  3144  spc2egv  3196  spc3egv  3198  relop  5158  elres  5314  en3  7777  en4  7778  addsrpr  9473  mulsrpr  9474  hash2prde  12516  hash2prv  12525  hash2sspr  12526  pmtrrn2  16485  usgrarnedg  24384  fundmpss  29196  pellexlem5  30769  fnchoice  31404  fzisoeu  31500  stoweidlem35  31817  stoweidlem60  31842  usgedgimp  32403  usgedgimpALT  32406  ax6e2eq  33330

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

This theorem depends on definitions:  df-bi 185  df-ex 1613