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

Theorem ralimia 3131
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 3130 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  wral 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905
This theorem depends on definitions:  df-bi 199  df-ral 3094
This theorem is referenced by:  ralimiaa  3132  ralimi  3133  r19.12  3244  rr19.3v  3535  rr19.28v  3536  exfo  6603  ffvresb  6620  f1mpt  6746  weniso  6832  ixpf  8170  ixpiunwdom  8738  tz9.12lem3  8902  dfac2a  9238  kmlem12  9271  axdc2lem  9558  ac6num  9589  ac6c4  9591  brdom6disj  9642  konigthlem  9678  arch  11577  cshw1  13907  serf0  14752  symgextfo  18154  baspartn  21087  ptcnplem  21753  spanuni  28928  lnopunilem1  29394  phpreu  33882  finixpnum  33883  poimirlem26  33924  indexa  34016  heiborlem5  34101  rngmgmbs4  34217  mzpincl  38079  dfac11  38413  stgoldbwt  42442  2zrngnmlid2  42746
  Copyright terms: Public domain W3C validator