MPE Home 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  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ral2imi  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch ) )

Proof of Theorem ral2imi
StepHypRef Expression
1 ral2imi.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21ralimi 2783 . 2  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ralim 2779 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  -> 
( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
42, 3syl 16 1  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.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