Theorem reximdv 2633

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

Syntax hints:   -> wi 4   e. wcel 2202   E.wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  r19.12  2639  reusv3  4557  rexxfrd  4560  iunpw  4577  fvelima  5697  carden2bex  7394  prnmaddl  7710  prarloclem5  7720  prarloc2  7724  genprndl  7741  genprndu  7742  ltpopr  7815  recexprlemm  7844  recexprlemopl  7845  recexprlemopu  7847  recexprlem1ssl  7853  recexprlem1ssu  7854  cauappcvgprlemupu  7869  caucvgprlemupu  7892  caucvgprprlemupu  7920  caucvgsrlemoffres  8020  map2psrprg  8025  resqrexlemgt0  11598  subcn2  11889  bezoutlembz  12593  pythagtriplem19  12873  mplsubgfileminv  14733  tgcl  14807  neiss  14893  ssnei2  14900  tgcnp  14952  cnptopco  14965  cnptopresti  14981  lmtopcnp  14993  blssexps  15172  blssex  15173  mopni3  15227  neibl  15234  metss  15237  metcnp3  15254  mpomulcn  15309  rescncf  15324  limcresi  15409  plyss  15481  umgrnloop0  15987  uhgr2edg  16076