Theorem ral2imi 2947

Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 2948. (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

Step	Hyp	Ref	Expression
1		df-ral 2917	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		ral2imi.1	. . . . 5 |- ( ph -> ( ps -> ch ) )
3	2	imim3i 64	. . . 4 |- ( ( x e. A -> ph ) -> ( ( x e. A -> ps ) -> ( x e. A -> ch ) ) )
4	3	al2imi 1743	. . 3 |- ( A. x ( x e. A -> ph ) -> ( A. x ( x e. A -> ps ) -> A. x ( x e. A -> ch ) ) )
5		df-ral 2917	. . 3 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
6		df-ral 2917	. . 3 |- ( A. x e. A ch <-> A. x ( x e. A -> ch ) )
7	4, 5, 6	3imtr4g 285	. 2 |- ( A. x ( x e. A -> ph ) -> ( A. x e. A ps -> A. x e. A ch ) )
8	1, 7	sylbi 207	1 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   A.wal 1481   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralim  2948  rexim  3008  r19.26  3064  iiner  7819  ss2ixp  7921  undifixp  7944  boxriin  7950  acni2  8869  axcc4  9261  intgru  9636  ingru  9637  prdsdsval3  16145  mrcmndind  17366  hauscmplem  21209  uspgr2wlkeq  26542  wlkp1lem8  26577  prdstotbnd  33593