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

Theorem ral2imi 2792
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 2791 . 2  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ralim 2787 . 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 setvar class
Syntax hints:    -> wi 4   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-ral 2720
This theorem is referenced by:  rexim  2820  r19.26  2849  iiner  7172  ss2ixp  7276  undifixp  7299  boxriin  7305  acni2  8216  axcc4  8608  intgru  8981  ingru  8982  prdsdsval3  14423  mrcmndind  15494  hauscmplem  19009  prdstotbnd  28693  usg2wlkeq  30289
  Copyright terms: Public domain W3C validator