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

Theorem ralimiaa 2980
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 449 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 2979 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 2946
This theorem is referenced by:  ralrnmpt  6408  tz7.48-2  7582  mptelixpg  7987  boxriin  7992  acnlem  8909  iundom2g  9400  konigthlem  9428  hashge2el2dif  13300  rlim2  14271  prdsbas3  16188  prdsdsval2  16191  ptbasfi  21432  ptunimpt  21446  voliun  23368  lgamgulmlem6  24805  riesz4i  29050  dmdbr6ati  29410
  Copyright terms: Public domain W3C validator