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