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

Metamath Proof Explorer

Theorem mpdi

Description: A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005) (Proof shortened by Mel L. O'Cat, 15-Jan-2008)

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

Proof

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