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

Theorem ralimia 3091
 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 3090 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2112  ∀wral 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812 This theorem depends on definitions:  df-bi 210  df-ral 3076 This theorem is referenced by:  ralimiaa  3092  ralimi  3093  rr19.3v  3583  rr19.28v  3584  exfo  6869  ffvresb  6886  f1mpt  7018  weniso  7108  ixpf  8516  ixpiunwdom  9101  tz9.12lem3  9265  dfac2a  9603  kmlem12  9635  axdc2lem  9922  ac6c4  9955  brdom6disj  10006  konigthlem  10042  arch  11945  cshw1  14245  serf0  15099  symgextfo  18632  baspartn  21669  ptcnplem  22336  spanuni  29441  lnopunilem1  29907  xpord2ind  33363  xpord3ind  33369  phpreu  35357  finixpnum  35358  poimirlem26  35399  indexa  35487  heiborlem5  35569  rngmgmbs4  35685  mzpincl  40094  dfac11  40425  mnurndlem1  41408  stgoldbwt  44721  2zrngnmlid2  45002
 Copyright terms: Public domain W3C validator