Metamath Proof Explorer

Theorem tposeqi

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

Ref Expression
Hypothesis tposeqi.1 
|- F = G
Assertion tposeqi 
|- tpos F = tpos G

Proof

Step Hyp Ref Expression
1 tposeqi.1 
 |-  F = G
2 tposeq 
 |-  ( F = G -> tpos F = tpos G )
3 1 2 ax-mp 
 |-  tpos F = tpos G