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	$$⊢\phi \to \forall x\psi$$
	bj-exlimd.th	$$⊢\phi \to \left(\exists x\theta \to \tau \right)$$
	bj-exlimd.maj	$$⊢\psi \to \left(\chi \to \theta \right)$$
Assertion	bj-exlimd	$$⊢\phi \to \left(\exists x\chi \to \tau \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-exlimd.ph	$$⊢\phi \to \forall x\psi$$
2		bj-exlimd.th	$$⊢\phi \to \left(\exists x\theta \to \tau \right)$$
3		bj-exlimd.maj	$$⊢\psi \to \left(\chi \to \theta \right)$$
4	1 3	sylg	$$⊢\phi \to \forall x\left(\chi \to \theta \right)$$
5		bj-exlimg	$$⊢\left(\exists x\theta \to \tau \right)\to \left(\forall x\left(\chi \to \theta \right)\to \left(\exists x\chi \to \tau \right)\right)$$
6	2 4 5	sylc	$$⊢\phi \to \left(\exists x\chi \to \tau \right)$$