Theorem sylanbrc

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		sylanbrc.1	$$⊢\phi \to \psi$$
2		sylanbrc.2	$$⊢\phi \to \chi$$
3		sylanbrc.3	$$⊢\theta \leftrightarrow \left(\psi \wedge \chi \right)$$
4	1 2	jca	$$⊢\phi \to \left(\psi \wedge \chi \right)$$
5	4 3	sylibr	$$⊢\phi \to \theta$$