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

Theorem ralimiaa 3082
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 414 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 3080 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3062
This theorem is referenced by:  ralrnmptw  7045  ralrnmpt  7047  tz7.48-2  8389  mptelixpg  8876  boxriin  8881  acnlem  9989  iundom2g  10481  konigthlem  10509  hashge2el2dif  14385  rlim2  15384  prdsbas3  17368  prdsdsval2  17371  ptbasfi  22948  ptunimpt  22962  voliun  24934  lgamgulmlem6  26399  riesz4i  31047  dmdbr6ati  31407  ctbssinf  35923
  Copyright terms: Public domain W3C validator