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

Metamath Proof Explorer

Theorem al2imi

Description: Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993)

Ref Expression
Hypothesis al2imi.1 ⊢ φ → ψ → χ
Assertion al2imi ⊢ ∀ x φ → ∀ x ψ → ∀ x χ

Proof

Step Hyp Ref Expression
1 al2imi.1 ⊢ φ → ψ → χ
2 al2im ⊢ ∀ x φ → ψ → χ → ∀ x φ → ∀ x ψ → ∀ x χ
3 2 1 mpg ⊢ ∀ x φ → ∀ x ψ → ∀ x χ