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

Metamath Proof Explorer

Theorem mp3an12i

Description: mp3an with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016)

Ref Expression
Hypotheses mp3an12i.1 ⊢ 𝜑
mp3an12i.2 ⊢ 𝜓
mp3an12i.3 ⊢ ( 𝜒 → 𝜃 )
mp3an12i.4 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜃 ) → 𝜏 )
Assertion mp3an12i ( 𝜒 → 𝜏 )

Proof

Step Hyp Ref Expression
1 mp3an12i.1 ⊢ 𝜑
2 mp3an12i.2 ⊢ 𝜓
3 mp3an12i.3 ⊢ ( 𝜒 → 𝜃 )
4 mp3an12i.4 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜃 ) → 𝜏 )
5 1 2 4 mp3an12 ⊢ ( 𝜃 → 𝜏 )
6 3 5 syl ⊢ ( 𝜒 → 𝜏 )