Theorem reximdv 2598

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

Ref	Expression
reximdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
reximdv	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		reximdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2597	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 2167   E.wrex 2476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  r19.12  2603  reusv3  4496  rexxfrd  4499  iunpw  4516  fvelima  5615  carden2bex  7268  prnmaddl  7574  prarloclem5  7584  prarloc2  7588  genprndl  7605  genprndu  7606  ltpopr  7679  recexprlemm  7708  recexprlemopl  7709  recexprlemopu  7711  recexprlem1ssl  7717  recexprlem1ssu  7718  cauappcvgprlemupu  7733  caucvgprlemupu  7756  caucvgprprlemupu  7784  caucvgsrlemoffres  7884  map2psrprg  7889  resqrexlemgt0  11202  subcn2  11493  bezoutlembz  12196  pythagtriplem19  12476  tgcl  14384  neiss  14470  ssnei2  14477  tgcnp  14529  cnptopco  14542  cnptopresti  14558  lmtopcnp  14570  blssexps  14749  blssex  14750  mopni3  14804  neibl  14811  metss  14814  metcnp3  14831  mpomulcn  14886  rescncf  14901  limcresi  14986  plyss  15058