Theorem ral2imi

Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006) Allow shortening of ralim . (Revised by Wolf Lammen, 1-Dec-2019)

	Ref	Expression
Hypothesis	ral2imi.1	|- ( ph -> ( ps -> ch ) )
Assertion	ral2imi	|- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ch ) )

Proof

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