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

Metamath Proof Explorer

Theorem mpii

Description: A doubly nested modus ponens inference. (Contributed by NM, 31-Dec-1993) (Proof shortened by Wolf Lammen, 31-Jul-2012)

Ref Expression
Hypotheses mpii.1 ⊢ χ
mpii.2 ⊢ φ → ψ → χ → θ
Assertion mpii ⊢ φ → ψ → θ

Proof

Step Hyp Ref Expression
1 mpii.1 ⊢ χ
2 mpii.2 ⊢ φ → ψ → χ → θ
3 1 a1i ⊢ ψ → χ
4 3 2 mpdi ⊢ φ → ψ → θ