**Description:** Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref | Expression | ||
---|---|---|---|

Hypothesis | tposeqd.1 | $${\u22a2}{\phi}\to {F}={G}$$ | |

Assertion | tposeqd | $${\u22a2}{\phi}\to tpos{F}=tpos{G}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | tposeqd.1 | $${\u22a2}{\phi}\to {F}={G}$$ | |

2 | tposeq | $${\u22a2}{F}={G}\to tpos{F}=tpos{G}$$ | |

3 | 1 2 | syl | $${\u22a2}{\phi}\to tpos{F}=tpos{G}$$ |