Theorem ralimdvva 3204

Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1807). (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 467	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))
3	2	ralimdva 3165	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 → ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralimdva 3165	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3060

This theorem is referenced by:  ralimdvv  3206  dedekindle  11423  isdomn4  20733  islmhm2  21055  dflidl2rng  21246  dmatscmcl  22525  cpmatacl  22738  cpmatinvcl  22739  mat2pmatf1  22751  pmatcollpw2lem  22799  tgpt0  24143  isngp4  24641  addcnlem  24900  c1lip3  26053  aalioulem2  26390  aalioulem5  26393  aalioulem6  26394  aaliou  26395  iscgrglt  28537  2pthfrgrrn  30311  2pthfrgrrn2  30312  equivbnd  37777  ghomco  37878  fcoresf1  47019  fullthinc  48846