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

Theorem ralimia 3080
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
ralimia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ralimia (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralimia
StepHypRef Expression
1 ralimia.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21a2i 14 . 2 ((𝑥𝐴𝜑) → (𝑥𝐴𝜓))
32ralimi2 3078 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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-ral 3062
This theorem is referenced by:  ralimiaa  3082  ralimi  3083  rr19.3v  3667  rr19.28v  3668  exfo  7125  ffvresb  7145  f1mpt  7281  weniso  7374  xpord2indlem  8172  ixpf  8960  ixpiunwdom  9630  tz9.12lem3  9829  dfac2a  10170  kmlem12  10202  axdc2lem  10488  ac6c4  10521  brdom6disj  10572  konigthlem  10608  arch  12523  cshw1  14860  serf0  15717  symgextfo  19440  baspartn  22961  ptcnplem  23629  spanuni  31563  lnopunilem1  32029  phpreu  37611  finixpnum  37612  poimirlem26  37653  indexa  37740  heiborlem5  37822  rngmgmbs4  37938  mzpincl  42745  dfac11  43074  mnurndlem1  44300  natlocalincr  46891  stgoldbwt  47763  2zrngnmlid2  48173
  Copyright terms: Public domain W3C validator