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

Theorem oteq3d 4088
Description: Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypothesis
Ref Expression
oteq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
oteq3d  |-  ( ph  -> 
<. C ,  D ,  A >.  =  <. C ,  D ,  B >. )

Proof of Theorem oteq3d
StepHypRef Expression
1 oteq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 oteq3 4085 . 2  |-  ( A  =  B  ->  <. C ,  D ,  A >.  = 
<. C ,  D ,  B >. )
31, 2syl 16 1  |-  ( ph  -> 
<. C ,  D ,  A >.  =  <. C ,  D ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   <.cotp 3900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2739  df-v 2989  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-ot 3901
This theorem is referenced by:  oteq123d  4089  idafval  14940  coafval  14947  arwlid  14955  arwrid  14956  arwass  14957  efgi  16231  efgtf  16234  efgtval  16235  efgval2  16236  mapdh6bN  35401  mapdh6cN  35402  mapdh6dN  35403  mapdh6gN  35406  hdmap1l6b  35476  hdmap1l6c  35477  hdmap1l6d  35478  hdmap1l6g  35481
  Copyright terms: Public domain W3C validator