Theorem bj-alrimd

Description: A slightly more general alrimd . A common usage will have ph substituted for ps and ch substituted for th , giving a form closer to alrimd . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Hypotheses	bj-alrimd.ph	|- ( ph -> A. x ps )
	bj-alrimd.th	|- ( ph -> ( ch -> A. x th ) )
	bj-alrimd.maj	|- ( ps -> ( th -> ta ) )
Assertion	bj-alrimd	|- ( ph -> ( ch -> A. x ta ) )

Proof

Step	Hyp	Ref	Expression
1		bj-alrimd.ph	|- ( ph -> A. x ps )
2		bj-alrimd.th	|- ( ph -> ( ch -> A. x th ) )
3		bj-alrimd.maj	|- ( ps -> ( th -> ta ) )
4	1 3	sylg	|- ( ph -> A. x ( th -> ta ) )
5		bj-alrimg	|- ( ( ch -> A. x th ) -> ( A. x ( th -> ta ) -> ( ch -> A. x ta ) ) )
6	2 4 5	sylc	|- ( ph -> ( ch -> A. x ta ) )