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 ⊢ θ