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

Theorem ral2imi 2852
Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 2853. (Revised by Wolf Lammen, 1-Dec-2019.)
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 df-ral 2819 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 ral2imi.1 . . . . 5  |-  ( ph  ->  ( ps  ->  ch ) )
32imim3i 59 . . . 4  |-  ( ( x  e.  A  ->  ph )  ->  ( ( x  e.  A  ->  ps )  ->  ( x  e.  A  ->  ch ) ) )
43al2imi 1616 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  A  ->  ch ) ) )
5 df-ral 2819 . . 3  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
6 df-ral 2819 . . 3  |-  ( A. x  e.  A  ch  <->  A. x ( x  e.  A  ->  ch )
)
74, 5, 63imtr4g 270 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
81, 7sylbi 195 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.wal 1377    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  ralim  2853  rexim  2929  r19.26  2989  iiner  7383  ss2ixp  7482  undifixp  7505  boxriin  7511  acni2  8426  axcc4  8818  intgru  9191  ingru  9192  prdsdsval3  14739  mrcmndind  15813  hauscmplem  19688  usg2wlkeq  24400  prdstotbnd  29909
  Copyright terms: Public domain W3C validator