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

Theorem ralimdvva 3205
Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1813). (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 469 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralimdva 3168 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 → ∀𝑦𝐵 𝜒))
43ralimdva 3168 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 → ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063
This theorem is referenced by:  ralimdvv  3207  dedekindle  11378  islmhm2  20649  dflidl2lem  20842  isdomn4  20918  dmatscmcl  22005  cpmatacl  22218  cpmatinvcl  22219  mat2pmatf1  22231  pmatcollpw2lem  22279  tgpt0  23623  isngp4  24121  addcnlem  24380  c1lip3  25516  aalioulem2  25846  aalioulem5  25849  aalioulem6  25850  aaliou  25851  iscgrglt  27765  2pthfrgrrn  29535  2pthfrgrrn2  29536  equivbnd  36658  ghomco  36759  fcoresf1  45779  dflidl2rng  46750  fullthinc  47666
  Copyright terms: Public domain W3C validator