Metamath Proof Explorer


Theorem frege108d

Description: If either A and C are the same or C follows A in the transitive closure of Rand B is the successor to C , then either A and B are the same or B follows A in the transitive closure of R . Similar to Proposition 108 of Frege1879 p. 74. Compare with frege108 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege108d.r φRV
frege108d.a φAV
frege108d.b φBV
frege108d.c φCV
frege108d.ac φAt+RCA=C
frege108d.cb φCRB
Assertion frege108d φAt+RBA=B

Proof

Step Hyp Ref Expression
1 frege108d.r φRV
2 frege108d.a φAV
3 frege108d.b φBV
4 frege108d.c φCV
5 frege108d.ac φAt+RCA=C
6 frege108d.cb φCRB
7 1 2 3 4 5 6 frege102d φAt+RB
8 7 frege106d φAt+RBA=B