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

Metamath Proof Explorer

Theorem mpid

Description: A nested modus ponens deduction. Deduction associated with mpi . (Contributed by NM, 14-Dec-2004)

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

Proof

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