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

Theorem ralimia 3163
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 3162 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3143
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 208  df-ral 3148
This theorem is referenced by:  ralimiaa  3164  ralimi  3165  r19.12OLD  3332  rr19.3v  3665  rr19.28v  3666  exfo  6869  ffvresb  6886  f1mpt  7015  weniso  7101  ixpf  8478  ixpiunwdom  9049  tz9.12lem3  9212  dfac2a  9549  kmlem12  9581  axdc2lem  9864  ac6c4  9897  brdom6disj  9948  konigthlem  9984  arch  11888  cshw1  14179  serf0  15032  symgextfo  18486  baspartn  21497  ptcnplem  22164  spanuni  29254  lnopunilem1  29720  phpreu  34762  finixpnum  34763  poimirlem26  34804  indexa  34895  heiborlem5  34980  rngmgmbs4  35096  mzpincl  39215  dfac11  39546  mnurndlem1  40501  stgoldbwt  43792  2zrngnmlid2  44124
  Copyright terms: Public domain W3C validator