Theorem mp4an

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		mp4an.1	⊢ 𝜑
2		mp4an.2	⊢ 𝜓
3		mp4an.3	⊢ 𝜒
4		mp4an.4	⊢ 𝜃
5		mp4an.5	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) → 𝜏 )
6	1 2	pm3.2i	⊢ ( 𝜑 ∧ 𝜓 )
7	3 4	pm3.2i	⊢ ( 𝜒 ∧ 𝜃 )
8	6 7 5	mp2an	⊢ 𝜏