This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mp3an13

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

Ref Expression
Hypotheses mp3an13.1 ⊢ φ
mp3an13.2 ⊢ χ
mp3an13.3 ⊢ φ ∧ ψ ∧ χ → θ
Assertion mp3an13 ⊢ ψ → θ

Proof

Step Hyp Ref Expression
1 mp3an13.1 ⊢ φ
2 mp3an13.2 ⊢ χ
3 mp3an13.3 ⊢ φ ∧ ψ ∧ χ → θ
4 2 3 mp3an3 ⊢ φ ∧ ψ → θ
5 1 4 mpan ⊢ ψ → θ