Theorem brcoi

Description: Ordered pair membership in a composition. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Hypotheses	brcoi.1	|- X e. _V
	brcoi.2	|- Y e. _V
	brcoi.3	|- Z e. _V
Assertion	brcoi	|- ( ( X R Y /\ Y S Z ) -> X ( S o. R ) Z )

Proof

Step	Hyp	Ref	Expression
1		brcoi.1	|- X e. _V
2		brcoi.2	|- Y e. _V
3		brcoi.3	|- Z e. _V
4	1 3 2	3pm3.2i	|- ( X e. _V /\ Z e. _V /\ Y e. _V )
5		brcogw	|- ( ( ( X e. _V /\ Z e. _V /\ Y e. _V ) /\ ( X R Y /\ Y S Z ) ) -> X ( S o. R ) Z )
6	4 5	mpan	|- ( ( X R Y /\ Y S Z ) -> X ( S o. R ) Z )