This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )