Theorem bj-alanim

Description: Closed form of alanimi . (Contributed by BJ, 6-May-2019)

	Ref	Expression
Assertion	bj-alanim	⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) → ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) → ∀ 𝑥 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		pm3.3	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) → ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
2	1	alimi	⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) → ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
3		al2im	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) )
4	2 3	syl	⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) → ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) ) )
5	4	impd	⊢ ( ∀ 𝑥 ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) → ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) → ∀ 𝑥 𝜒 ) )