Metamath Proof Explorer

Theorem bj-alanim

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

Ref Expression
Assertion bj-alanim ⊢ ∀ x φ ∧ ψ → χ → ∀ x φ ∧ ∀ x ψ → ∀ x χ

Proof

Step Hyp Ref Expression
1 pm3.3 ⊢ φ ∧ ψ → χ → φ → ψ → χ
2 1 alimi ⊢ ∀ x φ ∧ ψ → χ → ∀ x φ → ψ → χ
3 al2im ⊢ ∀ x φ → ψ → χ → ∀ x φ → ∀ x ψ → ∀ x χ
4 2 3 syl ⊢ ∀ x φ ∧ ψ → χ → ∀ x φ → ∀ x ψ → ∀ x χ
5 4 impd ⊢ ∀ x φ ∧ ψ → χ → ∀ x φ ∧ ∀ x ψ → ∀ x χ