Theorem eqeq2d 2241

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtrd  2262  eq2tri  2289  rspcedeq2vd  2917  rspceeqv  2925  sbceq1g  3144  euabsn  3736  absneu  3738  preq12bg  3850  cbvopab  4154  cbvopab1  4156  cbvopab2  4157  cbvopab1s  4158  cbvopab2v  4160  mpteq12f  4163  cbvmptf  4177  cbvmpt  4178  exmidsssn  4285  exmidsssnc  4286  opth  4322  eqvinop  4328  moop2  4337  euotd  4340  eusvnf  4543  reusv3i  4549  nlimsucg  4657  nn0suc  4695  opelxp  4748  elvvv  4781  relop  4871  elrnmpt1s  4973  elrnmpt1  4974  elsnres  5041  elxp4  5215  elxp5  5216  relresfld  5257  iotajust  5276  iota1  5292  iota2df  5303  funopg  5351  funcnvuni  5389  fun11iun  5592  funcocnv2  5596  nfvres  5662  ssimaex  5694  fvmptg  5709  fvmptdf  5721  fvopab6  5730  fnmptfvd  5738  fmptco  5800  fsng  5807  funopsn  5816  foco2  5876  elabrex  5880  elabrexg  5881  abrexco  5882  f1veqaeq  5892  dff13f  5893  f1ocnvfv  5902  f1ocnvfvb  5903  fcofo  5907  fliftfun  5919  fliftval  5923  f1oiso2  5950  riotaeqimp  5978  riota5f  5980  oprabid  6032  rspceov  6043  dfoprab2  6050  mpoeq123dva  6064  mpoeq3dva  6067  cbvoprab1  6075  cbvoprab2  6076  cbvoprab12  6077  cbvmpox  6081  mpomptx  6094  ovmpos  6127  ovmpodf  6135  ovmpodv2  6137  ovi3  6141  ov6g  6142  fnrnov  6150  foov  6151  caovcang  6166  caovcan  6169  f1opw2  6210  opabex3d  6264  opabex3  6265  fo1st  6301  fo2nd  6302  elxp6  6313  op1steq  6323  dfoprab4f  6337  fmpox  6344  fnmpoovd  6359  df1st2  6363  df2nd2  6364  xporderlem  6375  cnvoprab  6378  f1od2  6379  brtpos2  6395  dftpos4  6407  tposfn2  6410  recseq  6450  tfr1onlemaccex  6492  tfrcllemaccex  6505  frecabcl  6543  frecsuc  6551  nna0r  6622  eqerlem  6709  qseq2  6729  ecelqsg  6733  snec  6741  qsinxp  6756  ecoptocl  6767  eroveu  6771  th3qlem1  6782  th3qlem2  6783  th3q  6785  mapsncnv  6840  elixpsn  6880  ixpsnf1o  6881  en1  6949  mapsnen  6962  en2  6971  xpsnen  6976  xpassen  6985  pw2f1odclem  6991  xpf1o  7001  mapen  7003  mapxpen  7005  fidifsnen  7028  ac6sfi  7056  undifdc  7082  djuf1olem  7216  djur  7232  updjud  7245  omp1eomlem  7257  0ct  7270  enumctlemm  7277  fodjuomnilemdc  7307  fodjuomni  7312  fodjumkv  7323  nninfwlporlemd  7335  exmidfodomrlemeldju  7373  exmidfodomrlemreseldju  7374  cc2lem  7448  dfplpq2  7537  dfmpq2  7538  enqbreq2  7540  enq0sym  7615  enq0ref  7616  enq0tr  7617  addnq0mo  7630  mulnq0mo  7631  addnnnq0  7632  mulnnnq0  7633  nqnq0a  7637  nqnq0m  7638  nq0a0  7640  prarloclemcalc  7685  genipv  7692  genpassl  7707  genpassu  7708  addcomprg  7761  mulcomprg  7763  distrlem1prl  7765  distrlem1pru  7766  distrlem5prl  7769  distrlem5pru  7770  1idprl  7773  1idpru  7774  recexprlem1ssl  7816  recexprlem1ssu  7817  addsrmo  7926  mulsrmo  7927  addsrpr  7928  mulsrpr  7929  elreal  8011  axcnre  8064  axcaucvglemval  8080  negeu  8333  subeq0  8368  apreap  8730  apreim  8746  divmulap3  8820  diveqap0  8825  diveqap1  8848  nn0ind-raph  9560  elq  9813  zq  9817  elpq  9840  cnref1o  9842  iccf1o  10196  fzen  10235  fseq1m1p1  10287  fzm1  10292  modqmuladd  10583  modqmuladdnn0  10585  modfzo0difsn  10612  nn0ennn  10650  seqf1oglem1  10736  seq3id2  10743  qsqeqor  10867  bcval5  10980  fihashen1  11016  wrdl1exs1  11157  wrdl1s1  11158  wrd2ind  11250  swrdccatin2d  11271  reuccatpfxs1lem  11273  shftlem  11322  shftfvalg  11324  shftfval  11327  negfi  11734  xrmaxiflemcom  11755  xrnegiso  11768  xrnegcon1d  11770  sumeq2  11865  summodc  11889  fsum3  11893  fsum2dlemstep  11940  isumsplit  11997  mertenslemub  12040  mertensabs  12043  prodeq2w  12062  prodeq2  12063  prodmodc  12084  fprodseq  12089  fprod2dlemstep  12128  moddvds  12305  modm1div  12306  dvdsnegb  12314  dvdsabseq  12353  dvdsmod  12368  odd2np1lem  12378  odd2np1  12379  opeo  12403  omeo  12404  divalglemnn  12424  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  bitsinv1lem  12467  bezoutlemnewy  12512  bezoutlema  12515  bezoutlemb  12516  bezoutlemex  12517  bezoutlemaz  12519  bezoutlembz  12520  eucalglt  12574  qredeq  12613  qredeu  12614  divgcdcoprm0  12618  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  qnumdenbi  12709  hashgcdlem  12755  coprimeprodsq2  12776  pythagtriplem18  12799  pythagtriplem19  12800  pceu  12813  pcval  12814  pczpre  12815  pcdiv  12820  dvdsprmpweq  12853  dvdsprmpweqnn  12854  difsqpwdvds  12856  pcmpt  12861  pcfac  12868  oddprmdvds  12872  4sqlem2  12907  4sqlem3  12908  4sqlem4  12910  4sqlem12  12920  evenennn  12959  ennnfonelemim  12990  ptex  13292  intopsn  13395  igsumvalx  13417  gsumfzval  13419  gsumpropd  13420  gsumpropd2  13421  gsumress  13423  gsumval2  13425  ismnddef  13446  sgrpidmndm  13448  mndpfo  13466  mhmex  13490  grpid  13567  grpidrcan  13593  grpidlcan  13594  grplactcnv  13630  isghm  13775  f1ghm0to0  13804  conjghm  13808  srgpcomp  13948  ringadd2  13985  rrgval  14220  opprdomnbg  14232  islmod  14249  lss1d  14341  rspsn  14492  expghmap  14565  zndvds0  14608  znf1o  14609  mplvalcoe  14648  istopon  14681  eltg3  14725  restsn  14848  txuni2  14924  txopn  14933  upxp  14940  uptx  14942  txrest  14944  hmeoimaf1o  14982  xmettxlem  15177  xmettx  15178  elply2  15403  elplyr  15408  dvdsppwf1o  15657  mpodvdsmulf1o  15658  perfectlem2  15668  perfect  15669  lgslem1  15673  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem0i  15730  gausslemma2dlem1a  15731  gausslemma2d  15742  lgseisenlem2  15744  lgsquadlem2  15751  2lgslem1b  15762  2lgslem3a1  15770  2lgslem3b1  15771  2lgslem3c1  15772  2lgslem3d1  15773  2lgsoddprmlem2  15779  2sqlem2  15788  2sqlem8  15796  2sqlem9  15797  incistruhgr  15884  upgrex  15897  usgredg4  16007  usgredgreu  16008  uspgredg2vtxeu  16010  uspgredg2v  16013  usgredg2vlem2  16015  usgredg2v  16016  bj-nn0suc0  16271  bj-inf2vnlem1  16291  bj-nn0sucALT  16299  pwle2  16323  iooref1o  16361