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

Theorem ralimdvva 3176
Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1802). (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 468 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralimdva 3174 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 → ∀𝑦𝐵 𝜒))
43ralimdva 3174 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 → ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3140
This theorem is referenced by:  dedekindle  10792  islmhm2  19739  dmatscmcl  21040  cpmatacl  21252  cpmatinvcl  21253  mat2pmatf1  21265  pmatcollpw2lem  21313  tgpt0  22654  isngp4  23148  addcnlem  23399  c1lip3  24523  aalioulem2  24849  aalioulem5  24852  aalioulem6  24853  aaliou  24854  iscgrglt  26227  2pthfrgrrn  27988  2pthfrgrrn2  27989  equivbnd  34949  ghomco  35050
  Copyright terms: Public domain W3C validator