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