Theorem ralimdvva 3212

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3080

This theorem is used by:  ralimdvvOLD  3215  dedekindle  11484  isdomn4  20979  islmhm2  21325  dflidl2rng  21509  dmatscmcl  22830  cpmatacl  23046  cpmatinvcl  23047  mat2pmatf1  23059  pmatcollpw2lem  23107  tgpt0  24450  isngp4  24943  addcnlem  25196  c1lip3  26331  aalioulem2  26672  aalioulem5  26675  aalioulem6  26676  aaliou  26677  fltoprmgt3  28008  iscgrglt  28989  2pthfrgrrn  30895  2pthfrgrrn2  30896  equivbnd  38864  ghomco  38965  fcoresf1  48278  fullthinc  50724