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

Theorem ralimia 2947
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 2946 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wral 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-ral 2914
This theorem is referenced by:  ralimiaa  2948  ralimi  2949  r19.12  3059  rr19.3v  3339  rr19.28v  3340  exfo  6363  ffvresb  6380  f1mpt  6503  weniso  6589  ixpf  7915  ixpiunwdom  8481  tz9.12lem3  8637  dfac2a  8937  kmlem12  8968  axdc2lem  9255  ac6num  9286  ac6c4  9288  brdom6disj  9339  konigthlem  9375  arch  11274  cshw1  13549  serf0  14392  symgextfo  17823  baspartn  20739  ptcnplem  21405  spanuni  28373  lnopunilem1  28839  phpreu  33364  finixpnum  33365  poimirlem26  33406  indexa  33499  heiborlem5  33585  rngmgmbs4  33701  mzpincl  37116  dfac11  37451  stgoldbwt  41429  2zrngnmlid2  41716
  Copyright terms: Public domain W3C validator