Theorem bj-exlimd

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

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

Proof

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