Theorem rexlimdvva 2746

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

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

Assertion

Ref	Expression
rexlimdvva	|- (ph -> (E.x e. A E.y e. B ps -> ch))

Distinct variable groups:   x,y,ph   ch,x,y   y,A

Allowed substitution hints:   ps(x,y)   A(x)   B(x,y)

Proof of Theorem rexlimdvva

Step	Hyp	Ref	Expression
1		rexlimdvva.1	. . 3 |- ((ph /\ (x e. A /\ y e. B)) -> (ps -> ch))
2	1	ex 423	. 2 |- (ph -> ((x e. A /\ y e. B) -> (ps -> ch)))
3	2	rexlimdvv 2745	1 |- (ph -> (E.x e. A E.y e. B 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:  nnsucelr  4429  nndisjeq  4430  prepeano4  4452  ltfintr  4460  ncfinlower  4484  tfindi  4497  tfinsuc  4499  nnadjoin  4521  nnpweq  4524  sfindbl  4531  tfinnn  4535  vfinspsslem1  4551  ncdisjun  6137  peano4nc  6151  ncspw1eu  6160  ce0addcnnul  6180  sbth  6207  dflec2  6211  lectr  6212