Metamath Proof Explorer

Theorem tposeqd

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

Ref Expression
Hypothesis tposeqd.1 
|- ( ph -> F = G )
Assertion tposeqd 
|- ( ph -> tpos F = tpos G )

Proof

Step Hyp Ref Expression
1 tposeqd.1 
 |-  ( ph -> F = G )
2 tposeq 
 |-  ( F = G -> tpos F = tpos G )
3 1 2 syl 
 |-  ( ph -> tpos F = tpos G )