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

Theorem ral2imi 2811
Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 2812. (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 2778 . 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 1683 . . 3  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  A  ->  ch ) ) )
5 df-ral 2778 . . 3  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
6 df-ral 2778 . . 3  |-  ( A. x  e.  A  ch  <->  A. x ( x  e.  A  ->  ch )
)
74, 5, 63imtr4g 273 . 2  |-  ( A. x ( x  e.  A  ->  ph )  -> 
( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
81, 7sylbi 198 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 1435    e. wcel 1867   A.wral 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ral 2778
This theorem is referenced by:  ralim  2812  rexim  2888  r19.26  2953  iiner  7434  ss2ixp  7534  undifixp  7557  boxriin  7563  acni2  8466  axcc4  8858  intgru  9228  ingru  9229  prdsdsval3  15335  mrcmndind  16557  hauscmplem  20345  usg2wlkeq  25307  prdstotbnd  31859
  Copyright terms: Public domain W3C validator