Theorem ralimdvva 3181

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

Hypothesis

Ref	Expression
ralimdvva.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdvva	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝜑

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralimdvva

Step	Hyp	Ref	Expression
1		ralimdvva.1	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒))
2	1	anassrs 470	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))
3	2	ralimdva 3179	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 → ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralimdva 3179	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3145

This theorem is referenced by:  dedekindle  10806  islmhm2  19812  dmatscmcl  21114  cpmatacl  21326  cpmatinvcl  21327  mat2pmatf1  21339  pmatcollpw2lem  21387  tgpt0  22729  isngp4  23223  addcnlem  23474  c1lip3  24598  aalioulem2  24924  aalioulem5  24927  aalioulem6  24928  aaliou  24929  iscgrglt  26302  2pthfrgrrn  28063  2pthfrgrrn2  28064  equivbnd  35070  ghomco  35171