Theorem frege98d

Description: If C follows A and B follows C in the transitive closure of R , then B follows A in the transitive closure of R . Similar to Proposition 98 of Frege1879 p. 71. Compare with frege98 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypotheses	frege98d.a	|- ( ph -> A e. _V )
	frege98d.b	|- ( ph -> B e. _V )
	frege98d.c	|- ( ph -> C e. _V )
	frege98d.ac	|- ( ph -> A ( t+ ` R ) C )
	frege98d.cb	|- ( ph -> C ( t+ ` R ) B )
Assertion	frege98d	|- ( ph -> A ( t+ ` R ) B )

Proof

Step	Hyp	Ref	Expression
1		frege98d.a	|- ( ph -> A e. _V )
2		frege98d.b	|- ( ph -> B e. _V )
3		frege98d.c	|- ( ph -> C e. _V )
4		frege98d.ac	|- ( ph -> A ( t+ ` R ) C )
5		frege98d.cb	|- ( ph -> C ( t+ ` R ) B )
6		brcogw	|- ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ ( A ( t+ ` R ) C /\ C ( t+ ` R ) B ) ) -> A ( ( t+ ` R ) o. ( t+ ` R ) ) B )
7	1 2 3 4 5 6	syl32anc	|- ( ph -> A ( ( t+ ` R ) o. ( t+ ` R ) ) B )
8		trclfvcotrg	|- ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R )
9	8	a1i	|- ( ph -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )
10	9	ssbrd	|- ( ph -> ( A ( ( t+ ` R ) o. ( t+ ` R ) ) B -> A ( t+ ` R ) B ) )
11	7 10	mpd	|- ( ph -> A ( t+ ` R ) B )