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 𝐺