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

Theorem ralimiaa 3080
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 412 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 3078 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2106  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3060
This theorem is referenced by:  ralrnmptw  7114  ralrnmpt  7116  tz7.48-2  8481  mptelixpg  8974  boxriin  8979  acnlem  10086  iundom2g  10578  konigthlem  10606  hashge2el2dif  14516  rlim2  15529  prdsbas3  17528  prdsdsval2  17531  ptbasfi  23605  ptunimpt  23619  voliun  25603  lgamgulmlem6  27092  riesz4i  32092  dmdbr6ati  32452  ctbssinf  37389
  Copyright terms: Public domain W3C validator