Theorem mp4an

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

	Ref	Expression
Hypotheses	mp4an.1	$$⊢\phi$$
	mp4an.2	$$⊢\psi$$
	mp4an.3	$$⊢\chi$$
	mp4an.4	$$⊢\theta$$
	mp4an.5	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(\chi \wedge \theta \right)\right)\to \tau$$
Assertion	mp4an	$$⊢\tau$$

Proof

Step	Hyp	Ref	Expression
1		mp4an.1	$$⊢\phi$$
2		mp4an.2	$$⊢\psi$$
3		mp4an.3	$$⊢\chi$$
4		mp4an.4	$$⊢\theta$$
5		mp4an.5	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(\chi \wedge \theta \right)\right)\to \tau$$
6	1 2	pm3.2i	$$⊢\left(\phi \wedge \psi \right)$$
7	3 4	pm3.2i	$$⊢\left(\chi \wedge \theta \right)$$
8	6 7 5	mp2an	$$⊢\tau$$