MPE Home 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  |-  ( 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 2631 . 2  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ralim 2627 . 2  |-  ( A. x  e.  A  ( ps  ->  ch )  -> 
( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
42, 3syl 15 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 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