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

Theorem opeq1d 4062
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
Hypothesis
Ref Expression
opeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
opeq1d  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  C >. )

Proof of Theorem opeq1d
StepHypRef Expression
1 opeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 opeq1 4056 . 2  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
31, 2syl 16 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  C >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   <.cop 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881
This theorem is referenced by:  oteq1  4065  oteq2  4066  opth  4563  cbvoprab2  6158  unxpdomlem1  7513  mulcanenq  9125  ax1rid  9324  axrnegex  9325  fseq1m1p1  11531  uzrdglem  11776  swrd0swrd  12351  swrdccat  12380  swrdccat3a  12381  swrdccat3blem  12382  cshw0  12427  cshwmodn  12428  s2prop  12520  s4prop  12521  fsum2dlem  13233  ruclem1  13509  imasaddvallem  14463  iscatd2  14615  moni  14671  homadmcd  14906  curf1  15031  curf1cl  15034  curf2  15035  hofcl  15065  gsum2dlem2  16452  gsum2dOLD  16454  imasdsf1olem  19907  ovoliunlem1  20944  cxpcn3  22145  axlowdimlem15  23137  axlowdim  23142  nvi  23927  nvop  24000  phop  24153  br8d  25877  fgreu  25925  fprod2dlem  27420  br8  27495  fvtransport  27992  mat1dimmul  30755
  Copyright terms: Public domain W3C validator