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 467	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))
3	2	ralimdva 3146	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 → ∀𝑦 ∈ 𝐵 𝜒))
4	3	ralimdva 3146	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3049

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 207  df-an 396  df-ral 3050

This theorem is referenced by:  ralimdvvOLD  3184  dedekindle  11295  isdomn4  20647  islmhm2  20988  dflidl2rng  21171  dmatscmcl  22445  cpmatacl  22658  cpmatinvcl  22659  mat2pmatf1  22671  pmatcollpw2lem  22719  tgpt0  24061  isngp4  24554  addcnlem  24807  c1lip3  25958  aalioulem2  26295  aalioulem5  26298  aalioulem6  26299  aaliou  26300  iscgrglt  28535  2pthfrgrrn  30306  2pthfrgrrn2  30307  equivbnd  37930  ghomco  38031  fcoresf1  47257  fullthinc  49637