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

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