Theorem reximdv 2567

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

Syntax hints:   -> wi 4   e. wcel 2136   E.wrex 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449  df-rex 2450

This theorem is referenced by:  r19.12  2572  reusv3  4438  rexxfrd  4441  iunpw  4458  fvelima  5538  carden2bex  7145  prnmaddl  7431  prarloclem5  7441  prarloc2  7445  genprndl  7462  genprndu  7463  ltpopr  7536  recexprlemm  7565  recexprlemopl  7566  recexprlemopu  7568  recexprlem1ssl  7574  recexprlem1ssu  7575  cauappcvgprlemupu  7590  caucvgprlemupu  7613  caucvgprprlemupu  7641  caucvgsrlemoffres  7741  map2psrprg  7746  resqrexlemgt0  10962  subcn2  11252  bezoutlembz  11937  pythagtriplem19  12214  tgcl  12704  neiss  12790  ssnei2  12797  tgcnp  12849  cnptopco  12862  cnptopresti  12878  lmtopcnp  12890  blssexps  13069  blssex  13070  mopni3  13124  neibl  13131  metss  13134  metcnp3  13151  rescncf  13208  limcresi  13275