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 ⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )