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

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

Proof of Theorem oteq3
StepHypRef Expression
1 opeq2 4771 . 2 (𝐴 = 𝐵 → ⟨⟨𝐶, 𝐷⟩, 𝐴⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐵⟩)
2 df-ot 4535 . 2 𝐶, 𝐷, 𝐴⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐴
3 df-ot 4535 . 2 𝐶, 𝐷, 𝐵⟩ = ⟨⟨𝐶, 𝐷⟩, 𝐵
41, 2, 33eqtr4g 2799 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cop 4532  cotp 4534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858  df-sn 4527  df-pr 4529  df-op 4533  df-ot 4535
This theorem is referenced by:  oteq3d  4785  otsndisj  5386  otiunsndisj  5387  efgi0  18977  efgi1  18978  mapdhcl  39397  mapdh6dN  39409  mapdh8  39458  mapdh9a  39459  mapdh9aOLDN  39460  hdmap1l6d  39483  hdmapval  39498  hdmapval2  39502  hdmapval3N  39508  otiunsndisjX  44352
  Copyright terms: Public domain W3C validator