Theorem reximdv 2474

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

Syntax hints:   -> wi 4   e. wcel 1438   E.wrex 2360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364  df-rex 2365

This theorem is referenced by:  r19.12  2478  reusv3  4282  rexxfrd  4285  iunpw  4302  fvelima  5356  carden2bex  6817  prnmaddl  7049  prarloclem5  7059  prarloc2  7063  genprndl  7080  genprndu  7081  ltpopr  7154  recexprlemm  7183  recexprlemopl  7184  recexprlemopu  7186  recexprlem1ssl  7192  recexprlem1ssu  7193  cauappcvgprlemupu  7208  caucvgprlemupu  7231  caucvgprprlemupu  7259  caucvgsrlemoffres  7345  resqrexlemgt0  10453  subcn2  10700  bezoutlembz  11271  rescncf  11637