This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem al2im

Description: Closed form of al2imi . Version of alim for a nested implication. (Contributed by Alan Sare, 31-Dec-2011)

Ref Expression
Assertion al2im ⊢ ∀ x φ → ψ → χ → ∀ x φ → ∀ x ψ → ∀ x χ

Proof

Step Hyp Ref Expression
1 alim ⊢ ∀ x φ → ψ → χ → ∀ x φ → ∀ x ψ → χ
2 alim ⊢ ∀ x ψ → χ → ∀ x ψ → ∀ x χ
3 1 2 syl6 ⊢ ∀ x φ → ψ → χ → ∀ x φ → ∀ x ψ → ∀ x χ