Description: If B follows A in R , then either A and B are the same or B follows A in R . Similar to Proposition 106 of Frege1879 p. 73. Compare with frege106 . (Contributed by RP, 15-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | frege106d.cb | |- ( ph -> A R B ) |
|
| Assertion | frege106d | |- ( ph -> ( A R B \/ A = B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frege106d.cb | |- ( ph -> A R B ) |
|
| 2 | 1 | orcd | |- ( ph -> ( A R B \/ A = B ) ) |