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

Theorem ralimiaa 3081
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 3079 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2105  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810
This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3061
This theorem is referenced by:  ralrnmptw  7095  ralrnmpt  7097  tz7.48-2  8448  mptelixpg  8935  boxriin  8940  acnlem  10049  iundom2g  10541  konigthlem  10569  hashge2el2dif  14448  rlim2  15447  prdsbas3  17434  prdsdsval2  17437  ptbasfi  23404  ptunimpt  23418  voliun  25402  lgamgulmlem6  26878  riesz4i  31748  dmdbr6ati  32108  ctbssinf  36750
  Copyright terms: Public domain W3C validator