Theorem reximdv 2414

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

Syntax hints:   -> wi 4   e. wcel 1390  E.wrex 2301

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306

This theorem is referenced by:  r19.12  2416  reusv3  4158  rexxfrd  4161  iunpw  4177  fvelima  5168  prnmaddl  6473  prarloclem5  6483  prarloc2  6487  genprndl  6504  genprndu  6505  ltpopr  6569  recexprlemm  6596  recexprlemopl  6597  recexprlemopu  6599  recexprlem1ssl  6605  recexprlem1ssu  6606  cauappcvgprlemupu  6621  caucvgprlemupu  6643