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  4491  rexxfrd  4494  iunpw  4511  fvelima  5608  carden2bex  7249  prnmaddl  7550  prarloclem5  7560  prarloc2  7564  genprndl  7581  genprndu  7582  ltpopr  7655  recexprlemm  7684  recexprlemopl  7685  recexprlemopu  7687  recexprlem1ssl  7693  recexprlem1ssu  7694  cauappcvgprlemupu  7709  caucvgprlemupu  7732  caucvgprprlemupu  7760  caucvgsrlemoffres  7860  map2psrprg  7865  resqrexlemgt0  11164  subcn2  11454  bezoutlembz  12141  pythagtriplem19  12420  tgcl  14232  neiss  14318  ssnei2  14325  tgcnp  14377  cnptopco  14390  cnptopresti  14406  lmtopcnp  14418  blssexps  14597  blssex  14598  mopni3  14652  neibl  14659  metss  14662  metcnp3  14679  rescncf  14736  limcresi  14820  plyss  14884