Theorem reximdv 2507

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

Syntax hints:   -> wi 4   e. wcel 1463   E.wrex 2391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2395  df-rex 2396

This theorem is referenced by:  r19.12  2512  reusv3  4341  rexxfrd  4344  iunpw  4361  fvelima  5427  carden2bex  6995  prnmaddl  7246  prarloclem5  7256  prarloc2  7260  genprndl  7277  genprndu  7278  ltpopr  7351  recexprlemm  7380  recexprlemopl  7381  recexprlemopu  7383  recexprlem1ssl  7389  recexprlem1ssu  7390  cauappcvgprlemupu  7405  caucvgprlemupu  7428  caucvgprprlemupu  7456  caucvgsrlemoffres  7542  resqrexlemgt0  10684  subcn2  10972  bezoutlembz  11538  tgcl  12076  neiss  12162  ssnei2  12169  tgcnp  12220  cnptopco  12233  cnptopresti  12249  lmtopcnp  12261  blssexps  12418  blssex  12419  mopni3  12473  neibl  12480  metss  12483  metcnp3  12500  rescncf  12554  limcresi  12591