Theorem syl21anbrc

Description: Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022)

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

Proof

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