Metamath Proof Explorer


Theorem mpd3an23

Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006)

Ref Expression
Hypotheses mpd3an23.1 φψ
mpd3an23.2 φχ
mpd3an23.3 φψχθ
Assertion mpd3an23 φθ

Proof

Step Hyp Ref Expression
1 mpd3an23.1 φψ
2 mpd3an23.2 φχ
3 mpd3an23.3 φψχθ
4 id φφ
5 4 1 2 3 syl3anc φθ