Metamath Proof Explorer


Theorem mp3an

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999)

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

Proof

Step Hyp Ref Expression
1 mp3an.1 φ
2 mp3an.2 ψ
3 mp3an.3 χ
4 mp3an.4 φ ψ χ θ
5 1 4 mp3an1 ψ χ θ
6 2 3 5 mp2an θ