Theorem eqeq1i 2474

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	|- A = B

Assertion

Ref	Expression
eqeq1i	|- ( A = C <-> B = C )

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 |- A = B
2		eqeq1 2471	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	ax-mp 5	1 |- ( A = C <-> B = C )

Syntax hints:   <-> wb 184   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459

This theorem is referenced by:  eqeq12i  2487  neeq1i  2752  ssequn2  3677  dfss1  3703  dfss4  3732  disj  3867  disjr  3868  undisj1  3878  undisj2  3879  undif  3907  uneqdifeq  3915  reusn  4100  rabsneu  4102  eusn  4103  tppreqb  4168  uniintsn  4319  iin0  4621  opeqsn  4743  dfepfr  4864  epfrc  4865  unisuc  4954  dmopab3  5213  dm0rn0  5217  ssdmres  5293  imadisj  5354  args  5363  dffr3  5367  intirr  5383  dminxp  5445  dfrel3  5462  coeq0  5514  fntpg  5641  fncnv  5650  sbcfng  5726  f0rn0  5768  dff1o4  5822  dffv4  5861  fvun2  5937  fnreseql  5989  riota1  6262  riota2df  6264  fnotovb  6321  ovid  6401  ov  6404  ovg  6423  ovima0  6436  opiota  6840  tz7.49c  7108  sucprcreg  8021  sucprcregOLD  8022  inf3lem2  8042  zfregs2  8160  rankxpsuc  8296  scott0s  8302  cplem1  8303  cfslb2n  8644  fin23lem26  8701  dfacfin7  8775  axdc3lem4  8829  zorn2lem7  8878  alephom  8956  fpwwe2  9017  recmulnq  9338  recexsr  9480  map2psrpr  9483  renegcli  9876  elznn0  10875  xrsupss  11496  xrinfmss  11497  seqf1olem1  12110  seqf1olem2  12111  sqeqori  12244  hashrabsn1  12406  hashprb  12426  hashbclem  12463  hash2pwpr  12481  swrdccat3a  12678  f1oun2prg  12824  modfsummods  13566  cshwrepswhash1  14441  ismgmid  15748  oppgid  16186  lsmdisjr  16498  gexex  16652  dprd0  16868  oppr1  17067  opprunit  17094  opprdomn  17721  gsummoncoe1  18117  mat0dimcrng  18739  iinopn  19178  elcls  19340  ordthaus  19651  hauscmplem  19672  regr1lem2  19976  metdseq0  21093  minveclem1  21574  minveclem3b  21578  volun  21690  dyaddisj  21740  vieta1  22442  logeftb  22696  birthdaylem1  23009  lgseisenlem1  23352  rpvmasum  23439  axsegconlem6  23901  usgraedgprv  24052  wlkdvspthlem  24285  wlknwwlknsur  24388  wlkiswwlksur  24395  clwlkfclwwlk1hashn  24517  clwlkfoclwwlk  24521  1to3vfriswmgra  24683  frgrawopreg2  24728  rngosn3  25104  nmlno0lem  25384  minvecolem1  25466  hvsubeq0i  25656  hvsubaddi  25659  pjoc2i  26032  pjoml3i  26180  cmbr3i  26194  pjss2i  26274  hosubeq0i  26421  dmadjrnb  26501  nmlnop0iALT  26590  nmopcoadj0i  26698  stm1ri  26839  jplem2  26864  atoml2i  26978  chirredlem1  26985  cdj3lem3  27033  disjnf  27106  disjpreima  27118  disjunsn  27126  mptfnf  27171  f1od2  27219  addeq0  27230  zrhchr  27593  ddemeas  27848  braew  27854  aean  27856  eulerpartgbij  27951  eulerpartlemgh  27957  fib5  27984  fib6  27985  ballotlemfp1  28070  dmgmaddn0  28205  cvmsss2  28359  cvmlift2lem13  28400  elrn3  28769  br1steq  28781  br2ndeq  28782  sspred  28829  dffr4  28839  tz6.26  28862  wfi  28864  frind  28900  wfrlem8  28927  sltsolem1  29005  rankeq1o  29405  hfun  29412  tan2h  29624  asindmre  29679  totbndbnd  29888  scott0f  30181  iccdifioo  31119  fourierswlem  31531  fnresfnco  31678  afvpcfv0  31698  aovpcov0  31742  aov0ov0  31745  aovov0bi  31748  fnotaovb  31750  usgo0s0ALT  31905  usgo1s0ALT  31906  snlindsntor  32145  zfregs2VD  32721  bnj1143  32928  bj-pinftynminfty  33702  atbase  34086  llnbase  34305  lplnbase  34330  lvolbase  34374  lhpbase  34794  cdlemg31b0N  35490  cdlemg31b0a  35491  cdlemh  35613