Theorem ralimdvva 2964

Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1738). (Contributed by AV, 27-Nov-2019.)

Hypothesis

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

Assertion

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

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

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

Proof of Theorem ralimdvva

Step	Hyp	Ref	Expression
1		ralimdvva.1	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )
2	1	anassrs 680	. . 3 |- ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ps -> ch ) )
3	2	ralimdva 2962	. 2 |- ( ( ph /\ x e. A ) -> ( A. y e. B ps -> A. y e. B ch ) )
4	3	ralimdva 2962	1 |- ( ph -> ( A. x e. A A. y e. B ps -> A. x e. A A. y e. B ch ) )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  dedekindle  10201  islmhm2  19038  dmatscmcl  20309  cpmatacl  20521  cpmatinvcl  20522  mat2pmatf1  20534  pmatcollpw2lem  20582  tgpt0  21922  isngp4  22416  addcnlem  22667  c1lip3  23762  aalioulem2  24088  aalioulem5  24091  aalioulem6  24092  aaliou  24093  iscgrglt  25409  2pthfrgrrn  27146  2pthfrgrrn2  27147  equivbnd  33589  ghomco  33690