Theorem bj-alimdh

Description: General instance of alimdh . (Contributed by NM, 4-Jan-2002) State the most general derivable instance. (Revised by BJ, 5-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		bj-alimdh.nf	|- ( ph -> A. x ps )
2		bj-alimdh.maj	|- ( ps -> ( ch -> th ) )
3	2	al2imi	|- ( A. x ps -> ( A. x ch -> A. x th ) )
4	1 3	syl	|- ( ph -> ( A. x ch -> A. x th ) )