Metamath Proof Explorer


Theorem tposeqd

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

Ref Expression
Hypothesis tposeqd.1 φF=G
Assertion tposeqd φtposF=tposG

Proof

Step Hyp Ref Expression
1 tposeqd.1 φF=G
2 tposeq F=GtposF=tposG
3 1 2 syl φtposF=tposG