Description: Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | tposeqi.1 | ⊢ 𝐹 = 𝐺 | |
Assertion | tposeqi | ⊢ tpos 𝐹 = tpos 𝐺 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tposeqi.1 | ⊢ 𝐹 = 𝐺 | |
2 | tposeq | ⊢ ( 𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺 ) | |
3 | 1 2 | ax-mp | ⊢ tpos 𝐹 = tpos 𝐺 |