Theorem tposeqd

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

	Ref	Expression
Hypothesis	tposeqd.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
Assertion	tposeqd	⊢ ( 𝜑 → tpos 𝐹 = tpos 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		tposeqd.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
2		tposeq	⊢ ( 𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺 )
3	1 2	syl	⊢ ( 𝜑 → tpos 𝐹 = tpos 𝐺 )