Theorem eqeq2d 2182

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 2180	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqtrd  2203  eq2tri  2230  rspcedeq2vd  2844  rspceeqv  2852  sbceq1g  3069  euabsn  3653  absneu  3655  preq12bg  3760  cbvopab  4060  cbvopab1  4062  cbvopab2  4063  cbvopab1s  4064  cbvopab2v  4066  mpteq12f  4069  cbvmptf  4083  cbvmpt  4084  exmidsssn  4188  exmidsssnc  4189  opth  4222  eqvinop  4228  moop2  4236  euotd  4239  eusvnf  4438  reusv3i  4444  nlimsucg  4550  nn0suc  4588  opelxp  4641  elvvv  4674  relop  4761  elrnmpt1s  4861  elrnmpt1  4862  elsnres  4928  elxp4  5098  elxp5  5099  relresfld  5140  iotajust  5159  iota1  5174  iota2df  5184  funopg  5232  funcnvuni  5267  fun11iun  5463  funcocnv2  5467  nfvres  5529  ssimaex  5557  fvmptg  5572  fvmptdf  5583  fvopab6  5592  fnmptfvd  5600  fmptco  5662  fsng  5669  foco2  5733  elabrex  5737  abrexco  5738  f1veqaeq  5748  dff13f  5749  f1ocnvfv  5758  f1ocnvfvb  5759  fcofo  5763  fliftfun  5775  fliftval  5779  f1oiso2  5806  riota5f  5833  oprabid  5885  rspceov  5895  dfoprab2  5900  mpoeq123dva  5914  mpoeq3dva  5917  cbvoprab1  5925  cbvoprab2  5926  cbvoprab12  5927  cbvmpox  5931  mpomptx  5944  ovmpos  5976  ovmpodf  5984  ovmpodv2  5986  ovi3  5989  ov6g  5990  fnrnov  5998  foov  5999  caovcang  6014  caovcan  6017  f1opw2  6055  opabex3d  6100  opabex3  6101  fo1st  6136  fo2nd  6137  elxp6  6148  op1steq  6158  dfoprab4f  6172  fmpox  6179  fnmpoovd  6194  df1st2  6198  df2nd2  6199  xporderlem  6210  cnvoprab  6213  f1od2  6214  brtpos2  6230  dftpos4  6242  tposfn2  6245  recseq  6285  tfr1onlemaccex  6327  tfrcllemaccex  6340  frecabcl  6378  frecsuc  6386  nna0r  6457  eqerlem  6544  qseq2  6562  ecelqsg  6566  snec  6574  qsinxp  6589  ecoptocl  6600  eroveu  6604  th3qlem1  6615  th3qlem2  6616  th3q  6618  mapsncnv  6673  elixpsn  6713  ixpsnf1o  6714  en1  6777  mapsnen  6789  xpsnen  6799  xpassen  6808  xpf1o  6822  mapen  6824  mapxpen  6826  fidifsnen  6848  ac6sfi  6876  undifdc  6901  djuf1olem  7030  djur  7046  updjud  7059  omp1eomlem  7071  0ct  7084  enumctlemm  7091  fodjuomnilemdc  7120  fodjuomni  7125  fodjumkv  7136  nninfwlporlemd  7148  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  cc2lem  7228  dfplpq2  7316  dfmpq2  7317  enqbreq2  7319  enq0sym  7394  enq0ref  7395  enq0tr  7396  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  nqnq0a  7416  nqnq0m  7417  nq0a0  7419  prarloclemcalc  7464  genipv  7471  genpassl  7486  genpassu  7487  addcomprg  7540  mulcomprg  7542  distrlem1prl  7544  distrlem1pru  7545  distrlem5prl  7548  distrlem5pru  7549  1idprl  7552  1idpru  7553  recexprlem1ssl  7595  recexprlem1ssu  7596  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  elreal  7790  axcnre  7843  axcaucvglemval  7859  negeu  8110  subeq0  8145  apreap  8506  apreim  8522  divmulap3  8594  diveqap0  8599  diveqap1  8622  nn0ind-raph  9329  elq  9581  zq  9585  elpq  9607  cnref1o  9609  iccf1o  9961  fzen  9999  fseq1m1p1  10051  fzm1  10056  modqmuladd  10322  modqmuladdnn0  10324  modfzo0difsn  10351  nn0ennn  10389  seq3id2  10465  qsqeqor  10586  bcval5  10697  fihashen1  10734  shftlem  10780  shftfvalg  10782  shftfval  10785  negfi  11191  xrmaxiflemcom  11212  xrnegiso  11225  xrnegcon1d  11227  sumeq2  11322  summodc  11346  fsum3  11350  fsum2dlemstep  11397  isumsplit  11454  mertenslemub  11497  mertensabs  11500  prodeq2w  11519  prodeq2  11520  prodmodc  11541  fprodseq  11546  fprod2dlemstep  11585  moddvds  11761  modm1div  11762  dvdsnegb  11770  dvdsabseq  11807  dvdsmod  11822  odd2np1lem  11831  odd2np1  11832  opeo  11856  omeo  11857  divalglemnn  11877  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  bezoutlemnewy  11951  bezoutlema  11954  bezoutlemb  11955  bezoutlemex  11956  bezoutlemaz  11958  bezoutlembz  11959  eucalglt  12011  qredeq  12050  qredeu  12051  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  qnumdenbi  12146  hashgcdlem  12192  coprimeprodsq2  12212  pythagtriplem18  12235  pythagtriplem19  12236  pceu  12249  pcval  12250  pczpre  12251  pcdiv  12256  dvdsprmpweq  12288  dvdsprmpweqnn  12289  difsqpwdvds  12291  pcmpt  12295  pcfac  12302  oddprmdvds  12306  4sqlem2  12341  4sqlem3  12342  4sqlem4  12344  evenennn  12348  ennnfonelemim  12379  intopsn  12621  ismnddef  12654  sgrpidmndm  12656  mndpfo  12674  grpid  12742  grpidrcan  12764  grpidlcan  12765  istopon  12805  eltg3  12851  restsn  12974  txuni2  13050  txopn  13059  upxp  13066  uptx  13068  txrest  13070  hmeoimaf1o  13108  xmettxlem  13303  xmettx  13304  lgslem1  13695  lgsdirnn0  13742  lgsdinn0  13743  2sqlem2  13745  2sqlem8  13753  2sqlem9  13754  bj-nn0suc0  13985  bj-inf2vnlem1  14005  bj-nn0sucALT  14013  pwle2  14031  iooref1o  14066