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