Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralimdvva Structured version   Visualization version   GIF version

Theorem ralimdvva 3110
 Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1812). (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
StepHypRef Expression
1 ralimdvva.1 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
21anassrs 471 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralimdva 3108 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 → ∀𝑦𝐵 𝜒))
43ralimdva 3108 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 → ∀𝑥𝐴𝑦𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3075 This theorem is referenced by:  dedekindle  10842  islmhm2  19878  dmatscmcl  21203  cpmatacl  21416  cpmatinvcl  21417  mat2pmatf1  21429  pmatcollpw2lem  21477  tgpt0  22819  isngp4  23314  addcnlem  23565  c1lip3  24698  aalioulem2  25028  aalioulem5  25031  aalioulem6  25032  aaliou  25033  iscgrglt  26407  2pthfrgrrn  28166  2pthfrgrrn2  28167  equivbnd  35508  ghomco  35609
 Copyright terms: Public domain W3C validator