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

Theorem ral2imi 2632
 Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
Hypothesis
Ref Expression
ral2imi.1
Assertion
Ref Expression
ral2imi

Proof of Theorem ral2imi
StepHypRef Expression
1 ral2imi.1 . . 3
21ralimi 2631 . 2
3 ralim 2627 . 2
42, 3syl 15 1
 Colors of variables: wff set class Syntax hints:   wi 4  wral 2556 This theorem is referenced by:  rexim  2660  r19.26  2688  iiner  6747  ss2ixp  6845  undifixp  6868  boxriin  6874  acni2  7689  axcc4  8081  intgru  8452  ingru  8453  prdsdsval3  13400  hauscmplem  17149  cbicp  25269  inttop2  25618  intcont  25646  prdstotbnd  26621 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-ral 2561
 Copyright terms: Public domain W3C validator