Theorem reximdv 2565

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

Syntax hints:   -> wi 4   e. wcel 2135   E.wrex 2443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447  df-rex 2448

This theorem is referenced by:  r19.12  2570  reusv3  4432  rexxfrd  4435  iunpw  4452  fvelima  5532  carden2bex  7136  prnmaddl  7422  prarloclem5  7432  prarloc2  7436  genprndl  7453  genprndu  7454  ltpopr  7527  recexprlemm  7556  recexprlemopl  7557  recexprlemopu  7559  recexprlem1ssl  7565  recexprlem1ssu  7566  cauappcvgprlemupu  7581  caucvgprlemupu  7604  caucvgprprlemupu  7632  caucvgsrlemoffres  7732  map2psrprg  7737  resqrexlemgt0  10948  subcn2  11238  bezoutlembz  11922  pythagtriplem19  12191  tgcl  12605  neiss  12691  ssnei2  12698  tgcnp  12750  cnptopco  12763  cnptopresti  12779  lmtopcnp  12791  blssexps  12970  blssex  12971  mopni3  13025  neibl  13032  metss  13035  metcnp3  13052  rescncf  13109  limcresi  13176