Theorem syl22anbrc

Description: Syllogism inference. (Contributed by Thierry Arnoux, 19-Oct-2025)

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

Proof

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