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

Theorem oteq3d 4554
Description: Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypothesis
Ref Expression
oteq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
oteq3d (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)

Proof of Theorem oteq3d
StepHypRef Expression
1 oteq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 oteq3 4551 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐶, 𝐷, 𝐴⟩ = ⟨𝐶, 𝐷, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cotp 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-ot 4326
This theorem is referenced by:  oteq123d  4555  idafval  16914  coafval  16921  arwlid  16929  arwrid  16930  arwass  16931  efgi  18339  efgtf  18342  efgtval  18343  efgval2  18344  mapdh6bN  37547  mapdh6cN  37548  mapdh6dN  37549  mapdh6gN  37552  hdmap1l6b  37621  hdmap1l6c  37622  hdmap1l6d  37623  hdmap1l6g  37626
  Copyright terms: Public domain W3C validator