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

Theorem ral2imi 2784
 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 2783 . 2
3 ralim 2779 . 2
42, 3syl 16 1
 Colors of variables: wff set class Syntax hints:   wi 4  wral 2707 This theorem is referenced by:  rexim  2812  r19.26  2840  iiner  6978  ss2ixp  7077  undifixp  7100  boxriin  7106  acni2  7929  axcc4  8321  intgru  8691  ingru  8692  prdsdsval3  13709  hauscmplem  17471  prdstotbnd  26505  usg2wlkeq  28330 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567 This theorem depends on definitions:  df-bi 179  df-ral 2712
 Copyright terms: Public domain W3C validator