Theorem reximdv 2651

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

Syntax hints:   -> wi 4   e. wcel 2209   E.wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  r19.12  2657  reusv3  4601  rexxfrd  4604  iunpw  4621  fvelima  5748  carden2bex  7525  prnmaddl  7847  prarloclem5  7857  prarloc2  7861  genprndl  7878  genprndu  7879  ltpopr  7952  recexprlemm  7981  recexprlemopl  7982  recexprlemopu  7984  recexprlem1ssl  7990  recexprlem1ssu  7991  cauappcvgprlemupu  8006  caucvgprlemupu  8029  caucvgprprlemupu  8057  caucvgsrlemoffres  8157  map2psrprg  8162  resqrexlemgt0  11764  subcn2  12055  bezoutlembz  12759  pythagtriplem19  13039  mplsubgfileminv  15014  tgcl  15088  neiss  15174  ssnei2  15181  tgcnp  15233  cnptopco  15246  cnptopresti  15262  lmtopcnp  15274  blssexps  15453  blssex  15454  mopni3  15508  neibl  15515  metss  15518  metcnp3  15535  mpomulcn  15590  rescncf  15605  limcresi  15690  plyss  15762  umgrnloop0  16272  uhgr2edg  16361