Metamath Proof Explorer


Theorem frege91d

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 φ R V
frege91d.ac φ A R B
Assertion frege91d φ A t+ R B

Proof

Step Hyp Ref Expression
1 frege91d.r φ R V
2 frege91d.ac φ A R B
3 trclfvlb R V R t+ R
4 1 3 syl φ R t+ R
5 4 ssbrd φ A R B A t+ R B
6 2 5 mpd φ A t+ R B