Theorem bj-alrimdh

Description: Deduction form of Theorem 19.21 of Margaris p. 90, see 19.21 and 19.21h . (Contributed by NM, 10-Feb-1997) (Proof shortened by Andrew Salmon, 13-May-2011) State the most general derivable instance. (Revised by BJ, 5-Apr-2026)

	Ref	Expression
Hypotheses	bj-alrimdh.nf1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
	bj-alrimdh.nf2	⊢ ( 𝜒 → ∀ 𝑥 𝜃 )
	bj-alrimdh.maj	⊢ ( 𝜓 → ( 𝜃 → 𝜏 ) )
Assertion	bj-alrimdh	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-alrimdh.nf1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
2		bj-alrimdh.nf2	⊢ ( 𝜒 → ∀ 𝑥 𝜃 )
3		bj-alrimdh.maj	⊢ ( 𝜓 → ( 𝜃 → 𝜏 ) )
4	1 3	bj-alimdh	⊢ ( 𝜑 → ( ∀ 𝑥 𝜃 → ∀ 𝑥 𝜏 ) )
5	2 4	syl5	⊢ ( 𝜑 → ( 𝜒 → ∀ 𝑥 𝜏 ) )