MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oteq3 Structured version   Visualization version   GIF version

Theorem oteq3 4812
Description: Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
Assertion
Ref Expression
oteq3 (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)

Proof of Theorem oteq3
StepHypRef Expression
1 opeq2 4802 . 2 (𝐴 = 𝐵 → ⟨⟨𝐶, 𝐷⟩, 𝐴⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐵⟩)
2 df-ot 4572 . 2 𝐶, 𝐷, 𝐴⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐴
3 df-ot 4572 . 2 𝐶, 𝐷, 𝐵⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐵
41, 2, 33eqtr4g 2885 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  cop 4569  cotp 4571
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-ot 4572
This theorem is referenced by:  oteq3d  4815  otsndisj  5405  otiunsndisj  5406  efgi0  18768  efgi1  18769  mapdhcl  38732  mapdh6dN  38744  mapdh8  38793  mapdh9a  38794  mapdh9aOLDN  38795  hdmap1l6d  38818  hdmapval  38833  hdmapval2  38837  hdmapval3N  38843  otiunsndisjX  43346
  Copyright terms: Public domain W3C validator