Metamath Proof Explorer

Theorem mpd

Description: A modus ponens deduction. A translation of natural deduction rule -> E ( -> elimination), see natded . Deduction form of ax-mp . Inference associated with a2i . Commuted form of mpcom . (Contributed by NM, 29-Dec-1992)

Ref Expression
Hypotheses mpd.1 φ ψ
mpd.2 φ ψ χ
Assertion mpd φ χ


Step Hyp Ref Expression
1 mpd.1 φ ψ
2 mpd.2 φ ψ χ
3 2 a2i φ ψ φ χ
4 1 3 ax-mp φ χ