Theorem reximdv 2607

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

Syntax hints:   -> wi 4   e. wcel 2176   E.wrex 2485

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  r19.12  2612  reusv3  4508  rexxfrd  4511  iunpw  4528  fvelima  5632  carden2bex  7299  prnmaddl  7605  prarloclem5  7615  prarloc2  7619  genprndl  7636  genprndu  7637  ltpopr  7710  recexprlemm  7739  recexprlemopl  7740  recexprlemopu  7742  recexprlem1ssl  7748  recexprlem1ssu  7749  cauappcvgprlemupu  7764  caucvgprlemupu  7787  caucvgprprlemupu  7815  caucvgsrlemoffres  7915  map2psrprg  7920  resqrexlemgt0  11364  subcn2  11655  bezoutlembz  12358  pythagtriplem19  12638  mplsubgfileminv  14495  tgcl  14569  neiss  14655  ssnei2  14662  tgcnp  14714  cnptopco  14727  cnptopresti  14743  lmtopcnp  14755  blssexps  14934  blssex  14935  mopni3  14989  neibl  14996  metss  14999  metcnp3  15016  mpomulcn  15071  rescncf  15086  limcresi  15171  plyss  15243