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  8446  mptelixpg  8933  boxriin  8938  acnlem  10047  iundom2g  10539  konigthlem  10567  hashge2el2dif  14446  rlim2  15445  prdsbas3  17432  prdsdsval2  17435  ptbasfi  23306  ptunimpt  23320  voliun  25304  lgamgulmlem6  26775  riesz4i  31584  dmdbr6ati  31944  ctbssinf  36591
  Copyright terms: Public domain W3C validator