Theorem reximdv 2598

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

Syntax hints:   -> wi 4   e. wcel 2167   E.wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  r19.12  2603  reusv3  4495  rexxfrd  4498  iunpw  4515  fvelima  5612  carden2bex  7256  prnmaddl  7557  prarloclem5  7567  prarloc2  7571  genprndl  7588  genprndu  7589  ltpopr  7662  recexprlemm  7691  recexprlemopl  7692  recexprlemopu  7694  recexprlem1ssl  7700  recexprlem1ssu  7701  cauappcvgprlemupu  7716  caucvgprlemupu  7739  caucvgprprlemupu  7767  caucvgsrlemoffres  7867  map2psrprg  7872  resqrexlemgt0  11185  subcn2  11476  bezoutlembz  12171  pythagtriplem19  12451  tgcl  14300  neiss  14386  ssnei2  14393  tgcnp  14445  cnptopco  14458  cnptopresti  14474  lmtopcnp  14486  blssexps  14665  blssex  14666  mopni3  14720  neibl  14727  metss  14730  metcnp3  14747  mpomulcn  14802  rescncf  14817  limcresi  14902  plyss  14974