Theorem reximdv 2607

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

Syntax hints:   -> wi 4   e. wcel 2176   E.wrex 2485

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  r19.12  2612  reusv3  4507  rexxfrd  4510  iunpw  4527  fvelima  5630  carden2bex  7297  prnmaddl  7603  prarloclem5  7613  prarloc2  7617  genprndl  7634  genprndu  7635  ltpopr  7708  recexprlemm  7737  recexprlemopl  7738  recexprlemopu  7740  recexprlem1ssl  7746  recexprlem1ssu  7747  cauappcvgprlemupu  7762  caucvgprlemupu  7785  caucvgprprlemupu  7813  caucvgsrlemoffres  7913  map2psrprg  7918  resqrexlemgt0  11331  subcn2  11622  bezoutlembz  12325  pythagtriplem19  12605  mplsubgfileminv  14462  tgcl  14536  neiss  14622  ssnei2  14629  tgcnp  14681  cnptopco  14694  cnptopresti  14710  lmtopcnp  14722  blssexps  14901  blssex  14902  mopni3  14956  neibl  14963  metss  14966  metcnp3  14983  mpomulcn  15038  rescncf  15053  limcresi  15138  plyss  15210