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

Metamath Proof Explorer

Theorem mpd3an23

Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006)

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

Proof

Step Hyp Ref Expression
1 mpd3an23.1 ⊢ φ → ψ
2 mpd3an23.2 ⊢ φ → χ
3 mpd3an23.3 ⊢ φ ∧ ψ ∧ χ → θ
4 id ⊢ φ → φ
5 4 1 2 3 syl3anc ⊢ φ → θ