Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralimiaa Unicode version

Theorem ralimiaa 2630
 Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
ralimiaa.1
Assertion
Ref Expression
ralimiaa

Proof of Theorem ralimiaa
StepHypRef Expression
1 ralimiaa.1 . . 3
21ex 423 . 2
32ralimia 2629 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wcel 1696  wral 2556 This theorem is referenced by:  ralrnmpt  5685  tz7.48-2  6470  mptelixpg  6869  boxriin  6874  acnlem  7691  iundom2g  8178  konigthlem  8206  rlim2  11986  prdsbas3  13396  prdsdsval2  13399  ptbasfi  17292  ptunimpt  17306  voliun  18927  riesz4i  22659  dmdbr6ati  23019  srefwref  25170  fprodadd  25455  fprodneg  25481  fprodsub  25482  tartarmap  25991 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547 This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2561
 Copyright terms: Public domain W3C validator