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

Theorem ral2imi 2619
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 2618 . 2  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ralim 2614 . 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 2543
This theorem is referenced by:  rexim  2647  r19.26  2675  iiner  6731  ss2ixp  6829  undifixp  6852  boxriin  6858  acni2  7673  axcc4  8065  intgru  8436  ingru  8437  prdsdsval3  13384  hauscmplem  17133  cbicp  25166  inttop2  25515  intcont  25543  prdstotbnd  26518
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator