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

Theorem ralimiaa 3157
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 415 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 3156 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2107  wral 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3141
This theorem is referenced by:  ralrnmptw  6853  ralrnmpt  6855  tz7.48-2  8070  mptelixpg  8491  boxriin  8496  acnlem  9466  iundom2g  9954  konigthlem  9982  hashge2el2dif  13830  rlim2  14845  prdsbas3  16746  prdsdsval2  16749  ptbasfi  22181  ptunimpt  22195  voliun  24147  lgamgulmlem6  25603  riesz4i  29832  dmdbr6ati  30192  ctbssinf  34674
  Copyright terms: Public domain W3C validator