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

Theorem ral2imi 2788
Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 2789. (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 2754 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 ral2imi.1 . . . . 5  |-  ( ph  ->  ( ps  ->  ch ) )
32imim3i 61 . . . 4  |-  ( ( x  e.  A  ->  ph )  ->  ( ( x  e.  A  ->  ps )  ->  ( x  e.  A  ->  ch ) ) )
43al2imi 1698 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  A  ->  ch ) ) )
5 df-ral 2754 . . 3  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
6 df-ral 2754 . . 3  |-  ( A. x  e.  A  ch  <->  A. x ( x  e.  A  ->  ch )
)
74, 5, 63imtr4g 278 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
81, 7sylbi 200 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 1453    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693
This theorem depends on definitions:  df-bi 190  df-ral 2754
This theorem is referenced by:  ralim  2789  rexim  2864  r19.26  2929  iiner  7466  ss2ixp  7566  undifixp  7589  boxriin  7595  acni2  8508  axcc4  8900  intgru  9270  ingru  9271  prdsdsval3  15438  mrcmndind  16668  hauscmplem  20476  usg2wlkeq  25492  prdstotbnd  32172
  Copyright terms: Public domain W3C validator