Theorem eqeq2d 2216

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqeq2d	⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq2 2214	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197

This theorem is referenced by:  eqtrd  2237  eq2tri  2264  rspcedeq2vd  2886  rspceeqv  2894  sbceq1g  3112  euabsn  3702  absneu  3704  preq12bg  3813  cbvopab  4114  cbvopab1  4116  cbvopab2  4117  cbvopab1s  4118  cbvopab2v  4120  mpteq12f  4123  cbvmptf  4137  cbvmpt  4138  exmidsssn  4245  exmidsssnc  4246  opth  4280  eqvinop  4286  moop2  4294  euotd  4297  eusvnf  4498  reusv3i  4504  nlimsucg  4612  nn0suc  4650  opelxp  4703  elvvv  4736  relop  4826  elrnmpt1s  4926  elrnmpt1  4927  elsnres  4993  elxp4  5167  elxp5  5168  relresfld  5209  iotajust  5228  iota1  5243  iota2df  5254  funopg  5302  funcnvuni  5337  fun11iun  5537  funcocnv2  5541  nfvres  5604  ssimaex  5634  fvmptg  5649  fvmptdf  5661  fvopab6  5670  fnmptfvd  5678  fmptco  5740  fsng  5747  foco2  5812  elabrex  5816  elabrexg  5817  abrexco  5818  f1veqaeq  5828  dff13f  5829  f1ocnvfv  5838  f1ocnvfvb  5839  fcofo  5843  fliftfun  5855  fliftval  5859  f1oiso2  5886  riota5f  5914  oprabid  5966  rspceov  5977  dfoprab2  5982  mpoeq123dva  5996  mpoeq3dva  5999  cbvoprab1  6007  cbvoprab2  6008  cbvoprab12  6009  cbvmpox  6013  mpomptx  6026  ovmpos  6059  ovmpodf  6067  ovmpodv2  6069  ovi3  6073  ov6g  6074  fnrnov  6082  foov  6083  caovcang  6098  caovcan  6101  f1opw2  6142  opabex3d  6196  opabex3  6197  fo1st  6233  fo2nd  6234  elxp6  6245  op1steq  6255  dfoprab4f  6269  fmpox  6276  fnmpoovd  6291  df1st2  6295  df2nd2  6296  xporderlem  6307  cnvoprab  6310  f1od2  6311  brtpos2  6327  dftpos4  6339  tposfn2  6342  recseq  6382  tfr1onlemaccex  6424  tfrcllemaccex  6437  frecabcl  6475  frecsuc  6483  nna0r  6554  eqerlem  6641  qseq2  6661  ecelqsg  6665  snec  6673  qsinxp  6688  ecoptocl  6699  eroveu  6703  th3qlem1  6714  th3qlem2  6715  th3q  6717  mapsncnv  6772  elixpsn  6812  ixpsnf1o  6813  en1  6876  mapsnen  6888  xpsnen  6898  xpassen  6907  pw2f1odclem  6913  xpf1o  6923  mapen  6925  mapxpen  6927  fidifsnen  6949  ac6sfi  6977  undifdc  7003  djuf1olem  7137  djur  7153  updjud  7166  omp1eomlem  7178  0ct  7191  enumctlemm  7198  fodjuomnilemdc  7228  fodjuomni  7233  fodjumkv  7244  nninfwlporlemd  7256  exmidfodomrlemeldju  7289  exmidfodomrlemreseldju  7290  cc2lem  7360  dfplpq2  7449  dfmpq2  7450  enqbreq2  7452  enq0sym  7527  enq0ref  7528  enq0tr  7529  addnq0mo  7542  mulnq0mo  7543  addnnnq0  7544  mulnnnq0  7545  nqnq0a  7549  nqnq0m  7550  nq0a0  7552  prarloclemcalc  7597  genipv  7604  genpassl  7619  genpassu  7620  addcomprg  7673  mulcomprg  7675  distrlem1prl  7677  distrlem1pru  7678  distrlem5prl  7681  distrlem5pru  7682  1idprl  7685  1idpru  7686  recexprlem1ssl  7728  recexprlem1ssu  7729  addsrmo  7838  mulsrmo  7839  addsrpr  7840  mulsrpr  7841  elreal  7923  axcnre  7976  axcaucvglemval  7992  negeu  8245  subeq0  8280  apreap  8642  apreim  8658  divmulap3  8732  diveqap0  8737  diveqap1  8760  nn0ind-raph  9472  elq  9725  zq  9729  elpq  9752  cnref1o  9754  iccf1o  10108  fzen  10147  fseq1m1p1  10199  fzm1  10204  modqmuladd  10492  modqmuladdnn0  10494  modfzo0difsn  10521  nn0ennn  10559  seqf1oglem1  10645  seq3id2  10652  qsqeqor  10776  bcval5  10889  fihashen1  10925  shftlem  11046  shftfvalg  11048  shftfval  11051  negfi  11458  xrmaxiflemcom  11479  xrnegiso  11492  xrnegcon1d  11494  sumeq2  11589  summodc  11613  fsum3  11617  fsum2dlemstep  11664  isumsplit  11721  mertenslemub  11764  mertensabs  11767  prodeq2w  11786  prodeq2  11787  prodmodc  11808  fprodseq  11813  fprod2dlemstep  11852  moddvds  12029  modm1div  12030  dvdsnegb  12038  dvdsabseq  12077  dvdsmod  12092  odd2np1lem  12102  odd2np1  12103  opeo  12127  omeo  12128  divalglemnn  12148  divalglemeunn  12151  divalglemex  12152  divalglemeuneg  12153  bitsinv1lem  12191  bezoutlemnewy  12236  bezoutlema  12239  bezoutlemb  12240  bezoutlemex  12241  bezoutlemaz  12243  bezoutlembz  12244  eucalglt  12298  qredeq  12337  qredeu  12338  divgcdcoprm0  12342  divgcdcoprmex  12343  cncongr1  12344  cncongr2  12345  qnumdenbi  12433  hashgcdlem  12479  coprimeprodsq2  12500  pythagtriplem18  12523  pythagtriplem19  12524  pceu  12537  pcval  12538  pczpre  12539  pcdiv  12544  dvdsprmpweq  12577  dvdsprmpweqnn  12578  difsqpwdvds  12580  pcmpt  12585  pcfac  12592  oddprmdvds  12596  4sqlem2  12631  4sqlem3  12632  4sqlem4  12634  4sqlem12  12644  evenennn  12683  ennnfonelemim  12714  ptex  13014  intopsn  13117  igsumvalx  13139  gsumfzval  13141  gsumpropd  13142  gsumpropd2  13143  gsumress  13145  gsumval2  13147  ismnddef  13168  sgrpidmndm  13170  mndpfo  13188  mhmex  13212  grpid  13289  grpidrcan  13315  grpidlcan  13316  grplactcnv  13352  isghm  13497  f1ghm0to0  13526  conjghm  13530  srgpcomp  13670  ringadd2  13707  rrgval  13942  opprdomnbg  13954  islmod  13971  lss1d  14063  rspsn  14214  expghmap  14287  zndvds0  14330  znf1o  14331  mplvalcoe  14370  istopon  14403  eltg3  14447  restsn  14570  txuni2  14646  txopn  14655  upxp  14662  uptx  14664  txrest  14666  hmeoimaf1o  14704  xmettxlem  14899  xmettx  14900  elply2  15125  elplyr  15130  dvdsppwf1o  15379  mpodvdsmulf1o  15380  perfectlem2  15390  perfect  15391  lgslem1  15395  lgsdirnn0  15442  lgsdinn0  15443  gausslemma2dlem0i  15452  gausslemma2dlem1a  15453  gausslemma2d  15464  lgseisenlem2  15466  lgsquadlem2  15473  2lgslem1b  15484  2lgslem3a1  15492  2lgslem3b1  15493  2lgslem3c1  15494  2lgslem3d1  15495  2lgsoddprmlem2  15501  2sqlem2  15510  2sqlem8  15518  2sqlem9  15519  bj-nn0suc0  15750  bj-inf2vnlem1  15770  bj-nn0sucALT  15778  pwle2  15799  iooref1o  15837