Metamath Proof Explorer


Theorem mp3anl2

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

Ref Expression
Hypotheses mp3anl2.1 ψ
mp3anl2.2 φψχθτ
Assertion mp3anl2 φχθτ

Proof

Step Hyp Ref Expression
1 mp3anl2.1 ψ
2 mp3anl2.2 φψχθτ
3 2 ex φψχθτ
4 1 3 mp3an2 φχθτ
5 4 imp φχθτ