Theorem reximdv 2588

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 2587	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 2158   E.wrex 2466

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470  df-rex 2471

This theorem is referenced by:  r19.12  2593  reusv3  4472  rexxfrd  4475  iunpw  4492  fvelima  5580  carden2bex  7202  prnmaddl  7503  prarloclem5  7513  prarloc2  7517  genprndl  7534  genprndu  7535  ltpopr  7608  recexprlemm  7637  recexprlemopl  7638  recexprlemopu  7640  recexprlem1ssl  7646  recexprlem1ssu  7647  cauappcvgprlemupu  7662  caucvgprlemupu  7685  caucvgprprlemupu  7713  caucvgsrlemoffres  7813  map2psrprg  7818  resqrexlemgt0  11043  subcn2  11333  bezoutlembz  12019  pythagtriplem19  12296  tgcl  13917  neiss  14003  ssnei2  14010  tgcnp  14062  cnptopco  14075  cnptopresti  14091  lmtopcnp  14103  blssexps  14282  blssex  14283  mopni3  14337  neibl  14344  metss  14347  metcnp3  14364  rescncf  14421  limcresi  14488