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

Theorem ralimiaa 2935
 Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
ralimiaa.1 ((𝑥𝐴𝜑) → 𝜓)
Assertion
Ref Expression
ralimiaa (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralimiaa
StepHypRef Expression
1 ralimiaa.1 . . 3 ((𝑥𝐴𝜑) → 𝜓)
21ex 449 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 2934 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901 This theorem is referenced by:  ralrnmpt  6276  tz7.48-2  7424  mptelixpg  7831  boxriin  7836  acnlem  8754  iundom2g  9241  konigthlem  9269  hashge2el2dif  13117  rlim2  14075  prdsbas3  15964  prdsdsval2  15967  ptbasfi  21194  ptunimpt  21208  voliun  23129  lgamgulmlem6  24560  riesz4i  28306  dmdbr6ati  28666
 Copyright terms: Public domain W3C validator