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

Theorem ralimiaa 2849
 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 434 . 2
32ralimia 2848 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807 This theorem is referenced by:  ralrnmpt  6040  tz7.48-2  7126  mptelixpg  7526  boxriin  7531  acnlem  8450  iundom2g  8936  konigthlem  8964  hashge2el2dif  12521  rlim2  13319  prdsbas3  14878  prdsdsval2  14881  ptbasfi  20082  ptunimpt  20096  voliun  21964  riesz4i  26982  dmdbr6ati  27342  lgamgulmlem6  28576 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631 This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812
 Copyright terms: Public domain W3C validator