Theorem reximdv 2595

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

Syntax hints:   -> wi 4   e. wcel 2164   E.wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477  df-rex 2478

This theorem is referenced by:  r19.12  2600  reusv3  4492  rexxfrd  4495  iunpw  4512  fvelima  5609  carden2bex  7251  prnmaddl  7552  prarloclem5  7562  prarloc2  7566  genprndl  7583  genprndu  7584  ltpopr  7657  recexprlemm  7686  recexprlemopl  7687  recexprlemopu  7689  recexprlem1ssl  7695  recexprlem1ssu  7696  cauappcvgprlemupu  7711  caucvgprlemupu  7734  caucvgprprlemupu  7762  caucvgsrlemoffres  7862  map2psrprg  7867  resqrexlemgt0  11167  subcn2  11457  bezoutlembz  12144  pythagtriplem19  12423  tgcl  14243  neiss  14329  ssnei2  14336  tgcnp  14388  cnptopco  14401  cnptopresti  14417  lmtopcnp  14429  blssexps  14608  blssex  14609  mopni3  14663  neibl  14670  metss  14673  metcnp3  14690  mpomulcn  14745  rescncf  14760  limcresi  14845  plyss  14917