Metamath Proof Explorer


Theorem mp3an23

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

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

Proof

Step Hyp Ref Expression
1 mp3an23.1 ψ
2 mp3an23.2 χ
3 mp3an23.3 φ ψ χ θ
4 2 3 mp3an3 φ ψ θ
5 1 4 mpan2 φ θ