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	⊢ ( 𝜒 → 𝜏 )