Description: If B follows A in R then B follows A in the transitive closure of R . Similar to Proposition 91 of Frege1879 p. 68. Comparw with frege91 . (Contributed by RP, 15-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frege91d.r | ||
frege91d.ac | |||
Assertion | frege91d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege91d.r | ||
2 | frege91d.ac | ||
3 | trclfvlb | ||
4 | 1 3 | syl | |
5 | 4 | ssbrd | |
6 | 2 5 | mpd |