Metamath Proof Explorer


Theorem mp3anl3

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

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

Proof

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