Theorem reximdv 2609

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

Syntax hints:   -> wi 4   e. wcel 2178   E.wrex 2487

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491  df-rex 2492

This theorem is referenced by:  r19.12  2614  reusv3  4525  rexxfrd  4528  iunpw  4545  fvelima  5653  carden2bex  7323  prnmaddl  7638  prarloclem5  7648  prarloc2  7652  genprndl  7669  genprndu  7670  ltpopr  7743  recexprlemm  7772  recexprlemopl  7773  recexprlemopu  7775  recexprlem1ssl  7781  recexprlem1ssu  7782  cauappcvgprlemupu  7797  caucvgprlemupu  7820  caucvgprprlemupu  7848  caucvgsrlemoffres  7948  map2psrprg  7953  resqrexlemgt0  11446  subcn2  11737  bezoutlembz  12440  pythagtriplem19  12720  mplsubgfileminv  14577  tgcl  14651  neiss  14737  ssnei2  14744  tgcnp  14796  cnptopco  14809  cnptopresti  14825  lmtopcnp  14837  blssexps  15016  blssex  15017  mopni3  15071  neibl  15078  metss  15081  metcnp3  15098  mpomulcn  15153  rescncf  15168  limcresi  15253  plyss  15325