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

Theorem ralimiaa 3082
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 412 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 3080 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3062
This theorem is referenced by:  ralrnmptw  7114  ralrnmpt  7116  tz7.48-2  8482  mptelixpg  8975  boxriin  8980  acnlem  10088  iundom2g  10580  konigthlem  10608  hashge2el2dif  14519  rlim2  15532  prdsbas3  17526  prdsdsval2  17529  ptbasfi  23589  ptunimpt  23603  voliun  25589  lgamgulmlem6  27077  riesz4i  32082  dmdbr6ati  32442  ctbssinf  37407
  Copyright terms: Public domain W3C validator