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

Theorem ralimiaa 3132
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 403 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 3131 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  wcel 2106  wral 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853
This theorem depends on definitions:  df-bi 199  df-an 387  df-ral 3094
This theorem is referenced by:  ralrnmpt  6632  tz7.48-2  7820  mptelixpg  8231  boxriin  8236  acnlem  9204  iundom2g  9697  konigthlem  9725  hashge2el2dif  13576  rlim2  14635  prdsbas3  16527  prdsdsval2  16530  ptbasfi  21793  ptunimpt  21807  voliun  23758  lgamgulmlem6  25212  riesz4i  29494  dmdbr6ati  29854
  Copyright terms: Public domain W3C validator