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 ⊢ ( 𝜑 → 𝜃 )