Theorem tposeqd

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

	Ref	Expression
Hypothesis	tposeqd.1	$$⊢\phi \to F=G$$
Assertion	tposeqd	$$⊢\phi \to tposF=tposG$$

Proof

Step	Hyp	Ref	Expression
1		tposeqd.1	$$⊢\phi \to F=G$$
2		tposeq	$$⊢F=G\to tposF=tposG$$
3	1 2	syl	$$⊢\phi \to tposF=tposG$$