Metamath Proof Explorer


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 φAV
frege98d.b φBV
frege98d.c φCV
frege98d.ac φAt+RC
frege98d.cb φCt+RB
Assertion frege98d φAt+RB

Proof

Step Hyp Ref Expression
1 frege98d.a φAV
2 frege98d.b φBV
3 frege98d.c φCV
4 frege98d.ac φAt+RC
5 frege98d.cb φCt+RB
6 brcogw AVBVCVAt+RCCt+RBAt+Rt+RB
7 1 2 3 4 5 6 syl32anc φAt+Rt+RB
8 trclfvcotrg t+Rt+Rt+R
9 8 a1i φt+Rt+Rt+R
10 9 ssbrd φAt+Rt+RBAt+RB
11 7 10 mpd φAt+RB