Metamath Proof Explorer


Theorem tposeqi

Description: Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis tposeqi.1 𝐹 = 𝐺
Assertion tposeqi tpos 𝐹 = tpos 𝐺

Proof

Step Hyp Ref Expression
1 tposeqi.1 𝐹 = 𝐺
2 tposeq ( 𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺 )
3 1 2 ax-mp tpos 𝐹 = tpos 𝐺