Theorem sylan

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 22-Nov-2012)

	Ref	Expression
Hypotheses	sylan.1	$$⊢\phi \to \psi$$
	sylan.2	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
Assertion	sylan	$$⊢\left(\phi \wedge \chi \right)\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		sylan.1	$$⊢\phi \to \psi$$
2		sylan.2	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
3	2	expcom	$$⊢\chi \to \left(\psi \to \theta \right)$$
4	1 3	mpan9	$$⊢\left(\phi \wedge \chi \right)\to \theta$$