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

Theorem ralimdvva 3202
Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1810). (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 466 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralimdva 3165 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 → ∀𝑦𝐵 𝜒))
43ralimdva 3165 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 → ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2104  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911
This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060
This theorem is referenced by:  ralimdvv  3204  dedekindle  11382  islmhm2  20793  dflidl2lem  20991  dflidl2rng  21030  isdomn4  21118  dmatscmcl  22225  cpmatacl  22438  cpmatinvcl  22439  mat2pmatf1  22451  pmatcollpw2lem  22499  tgpt0  23843  isngp4  24341  addcnlem  24600  c1lip3  25751  aalioulem2  26082  aalioulem5  26085  aalioulem6  26086  aaliou  26087  iscgrglt  28032  2pthfrgrrn  29802  2pthfrgrrn2  29803  equivbnd  36961  ghomco  37062  fcoresf1  46077  fullthinc  47753
  Copyright terms: Public domain W3C validator