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

Proof

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