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

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