Theorem rexlimdva 2739

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	|- ((ph /\ x e. A) -> (ps -> ch))

Assertion

Ref	Expression
rexlimdva	|- (ph -> (E.x e. A ps -> ch))

Distinct variable groups:   ph,x   ch,x

Allowed substitution hints:   ps(x)   A(x)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 |- ((ph /\ x e. A) -> (ps -> ch))
2	1	ex 423	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	2	rexlimdv 2738	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 4   /\ wa 358   e. wcel 1710  E.wrex 2616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2620  df-rex 2621

This theorem is referenced by:  rexlimdvaa  2740  rexlimivv  2744  rexlimdvv  2745  pw1disj  4168  leltfintr  4459  ncfinlower  4484  tfin11  4494  tfinpw1  4495  nnpweq  4524  sfin112  4530  sfindbl  4531  vfinspss  4552  vfinspeqtncv  4554  phi11lem1  4596  foco2  5427  f1elima  5475  ectocld  5992  ncssfin  6152  nntccl  6171  dflec2  6211  leaddc1  6215  leconnnc  6219  tlecg  6231  letc  6232  ce2le  6234  ce0lenc1  6240  nclenn  6250  lemuc1  6254  lecadd2  6267  ncslesuc  6268  nnc3n3p1  6279  nchoicelem17  6306  nchoicelem19  6308  nchoice  6309  dmfrec  6317  fnfreclem3  6320