Theorem oteq3 4889

Description: Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)

Assertion

Ref	Expression
oteq3	⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)

Proof of Theorem oteq3

Step	Hyp	Ref	Expression
1		opeq2 4879	. 2 ⊢ (𝐴 = 𝐵 → ⟨⟨𝐶, 𝐷⟩, 𝐴⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐵⟩)
2		df-ot 4641	. 2 ⊢ ⟨𝐶, 𝐷, 𝐴⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐴⟩
3		df-ot 4641	. 2 ⊢ ⟨𝐶, 𝐷, 𝐵⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐵⟩
4	1, 2, 3	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)

Syntax hints:   → wi 4   = wceq 1533  ⟨cop 4638  ⟨cotp 4640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-ot 4641

This theorem is referenced by:  oteq3d  4892  otsndisj  5525  otiunsndisj  5526  xpord3pred  8163  efgi0  19682  efgi1  19683  mapdhcl  41232  mapdh6dN  41244  mapdh8  41293  mapdh9a  41294  mapdh9aOLDN  41295  hdmap1l6d  41318  hdmapval  41333  hdmapval2  41337  hdmapval3N  41343  otiunsndisjX  46688