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

Theorem ralimiaa 2946
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 450 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 2945 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  wral 2907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2912
This theorem is referenced by:  ralrnmpt  6329  tz7.48-2  7489  mptelixpg  7896  boxriin  7901  acnlem  8822  iundom2g  9313  konigthlem  9341  hashge2el2dif  13207  rlim2  14168  prdsbas3  16069  prdsdsval2  16072  ptbasfi  21303  ptunimpt  21317  voliun  23241  lgamgulmlem6  24673  riesz4i  28789  dmdbr6ati  29149
  Copyright terms: Public domain W3C validator