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

Theorem ralimdvva 3113
Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1886). (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 458 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralimdva 3111 . 2 ((𝜑𝑥𝐴) → (∀𝑦𝐵 𝜓 → ∀𝑦𝐵 𝜒))
43ralimdva 3111 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 → ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ral 3066
This theorem is referenced by:  dedekindle  10403  islmhm2  19251  dmatscmcl  20527  cpmatacl  20741  cpmatinvcl  20742  mat2pmatf1  20754  pmatcollpw2lem  20802  tgpt0  22142  isngp4  22636  addcnlem  22887  c1lip3  23982  aalioulem2  24308  aalioulem5  24311  aalioulem6  24312  aaliou  24313  iscgrglt  25630  2pthfrgrrn  27464  2pthfrgrrn2  27465  equivbnd  33921  ghomco  34022
  Copyright terms: Public domain W3C validator