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

Theorem ralimiaa 3086
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 416 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 3085 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  wral 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817
This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3069
This theorem is referenced by:  ralrnmptw  6935  ralrnmpt  6937  tz7.48-2  8202  mptelixpg  8640  boxriin  8645  acnlem  9692  iundom2g  10184  konigthlem  10212  hashge2el2dif  14079  rlim2  15090  prdsbas3  17019  prdsdsval2  17022  ptbasfi  22510  ptunimpt  22524  voliun  24483  lgamgulmlem6  25948  riesz4i  30176  dmdbr6ati  30536  ctbssinf  35351
  Copyright terms: Public domain W3C validator