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	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
	bj-alrimd.th	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜃 ) )
	bj-alrimd.maj	⊢ ( 𝜓 → ( 𝜃 → 𝜏 ) )
Assertion	bj-alrimd	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-alrimd.ph	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
2		bj-alrimd.th	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜃 ) )
3		bj-alrimd.maj	⊢ ( 𝜓 → ( 𝜃 → 𝜏 ) )
4	1 3	sylg	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜃 → 𝜏 ) )
5		bj-alrimg	⊢ ( ( 𝜒 → ∀ 𝑥 𝜃 ) → ( ∀ 𝑥 ( 𝜃 → 𝜏 ) → ( 𝜒 → ∀ 𝑥 𝜏 ) ) )
6	2 4 5	sylc	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜏 ) )