Theorem reximdv 2420

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

Syntax hints:   -> wi 4   e. wcel 1393   E.wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312

This theorem is referenced by:  r19.12  2422  reusv3  4192  rexxfrd  4195  iunpw  4211  fvelima  5225  carden2bex  6369  prnmaddl  6588  prarloclem5  6598  prarloc2  6602  genprndl  6619  genprndu  6620  ltpopr  6693  recexprlemm  6722  recexprlemopl  6723  recexprlemopu  6725  recexprlem1ssl  6731  recexprlem1ssu  6732  cauappcvgprlemupu  6747  caucvgprlemupu  6770  caucvgprprlemupu  6798  caucvgsrlemoffres  6884  resqrexlemgt0  9618  subcn2  9832