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

Proof

Step	Hyp	Ref	Expression
1		bj-alimdh.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
2		bj-alimdh.maj	⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
3	2	al2imi	⊢ ( ∀ 𝑥 𝜓 → ( ∀ 𝑥 𝜒 → ∀ 𝑥 𝜃 ) )
4	1 3	syl	⊢ ( 𝜑 → ( ∀ 𝑥 𝜒 → ∀ 𝑥 𝜃 ) )