Theorem eqeq2d 2218

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqtrd  2239  eq2tri  2266  rspcedeq2vd  2891  rspceeqv  2899  sbceq1g  3117  euabsn  3708  absneu  3710  preq12bg  3820  cbvopab  4123  cbvopab1  4125  cbvopab2  4126  cbvopab1s  4127  cbvopab2v  4129  mpteq12f  4132  cbvmptf  4146  cbvmpt  4147  exmidsssn  4254  exmidsssnc  4255  opth  4289  eqvinop  4295  moop2  4304  euotd  4307  eusvnf  4508  reusv3i  4514  nlimsucg  4622  nn0suc  4660  opelxp  4713  elvvv  4746  relop  4836  elrnmpt1s  4937  elrnmpt1  4938  elsnres  5005  elxp4  5179  elxp5  5180  relresfld  5221  iotajust  5240  iota1  5255  iota2df  5266  funopg  5314  funcnvuni  5352  fun11iun  5555  funcocnv2  5559  nfvres  5623  ssimaex  5653  fvmptg  5668  fvmptdf  5680  fvopab6  5689  fnmptfvd  5697  fmptco  5759  fsng  5766  funopsn  5775  foco2  5835  elabrex  5839  elabrexg  5840  abrexco  5841  f1veqaeq  5851  dff13f  5852  f1ocnvfv  5861  f1ocnvfvb  5862  fcofo  5866  fliftfun  5878  fliftval  5882  f1oiso2  5909  riota5f  5937  oprabid  5989  rspceov  6000  dfoprab2  6005  mpoeq123dva  6019  mpoeq3dva  6022  cbvoprab1  6030  cbvoprab2  6031  cbvoprab12  6032  cbvmpox  6036  mpomptx  6049  ovmpos  6082  ovmpodf  6090  ovmpodv2  6092  ovi3  6096  ov6g  6097  fnrnov  6105  foov  6106  caovcang  6121  caovcan  6124  f1opw2  6165  opabex3d  6219  opabex3  6220  fo1st  6256  fo2nd  6257  elxp6  6268  op1steq  6278  dfoprab4f  6292  fmpox  6299  fnmpoovd  6314  df1st2  6318  df2nd2  6319  xporderlem  6330  cnvoprab  6333  f1od2  6334  brtpos2  6350  dftpos4  6362  tposfn2  6365  recseq  6405  tfr1onlemaccex  6447  tfrcllemaccex  6460  frecabcl  6498  frecsuc  6506  nna0r  6577  eqerlem  6664  qseq2  6684  ecelqsg  6688  snec  6696  qsinxp  6711  ecoptocl  6722  eroveu  6726  th3qlem1  6737  th3qlem2  6738  th3q  6740  mapsncnv  6795  elixpsn  6835  ixpsnf1o  6836  en1  6904  mapsnen  6917  en2  6926  xpsnen  6931  xpassen  6940  pw2f1odclem  6946  xpf1o  6956  mapen  6958  mapxpen  6960  fidifsnen  6982  ac6sfi  7010  undifdc  7036  djuf1olem  7170  djur  7186  updjud  7199  omp1eomlem  7211  0ct  7224  enumctlemm  7231  fodjuomnilemdc  7261  fodjuomni  7266  fodjumkv  7277  nninfwlporlemd  7289  exmidfodomrlemeldju  7323  exmidfodomrlemreseldju  7324  cc2lem  7398  dfplpq2  7487  dfmpq2  7488  enqbreq2  7490  enq0sym  7565  enq0ref  7566  enq0tr  7567  addnq0mo  7580  mulnq0mo  7581  addnnnq0  7582  mulnnnq0  7583  nqnq0a  7587  nqnq0m  7588  nq0a0  7590  prarloclemcalc  7635  genipv  7642  genpassl  7657  genpassu  7658  addcomprg  7711  mulcomprg  7713  distrlem1prl  7715  distrlem1pru  7716  distrlem5prl  7719  distrlem5pru  7720  1idprl  7723  1idpru  7724  recexprlem1ssl  7766  recexprlem1ssu  7767  addsrmo  7876  mulsrmo  7877  addsrpr  7878  mulsrpr  7879  elreal  7961  axcnre  8014  axcaucvglemval  8030  negeu  8283  subeq0  8318  apreap  8680  apreim  8696  divmulap3  8770  diveqap0  8775  diveqap1  8798  nn0ind-raph  9510  elq  9763  zq  9767  elpq  9790  cnref1o  9792  iccf1o  10146  fzen  10185  fseq1m1p1  10237  fzm1  10242  modqmuladd  10533  modqmuladdnn0  10535  modfzo0difsn  10562  nn0ennn  10600  seqf1oglem1  10686  seq3id2  10693  qsqeqor  10817  bcval5  10930  fihashen1  10966  wrdl1exs1  11106  wrdl1s1  11107  wrd2ind  11199  shftlem  11202  shftfvalg  11204  shftfval  11207  negfi  11614  xrmaxiflemcom  11635  xrnegiso  11648  xrnegcon1d  11650  sumeq2  11745  summodc  11769  fsum3  11773  fsum2dlemstep  11820  isumsplit  11877  mertenslemub  11920  mertensabs  11923  prodeq2w  11942  prodeq2  11943  prodmodc  11964  fprodseq  11969  fprod2dlemstep  12008  moddvds  12185  modm1div  12186  dvdsnegb  12194  dvdsabseq  12233  dvdsmod  12248  odd2np1lem  12258  odd2np1  12259  opeo  12283  omeo  12284  divalglemnn  12304  divalglemeunn  12307  divalglemex  12308  divalglemeuneg  12309  bitsinv1lem  12347  bezoutlemnewy  12392  bezoutlema  12395  bezoutlemb  12396  bezoutlemex  12397  bezoutlemaz  12399  bezoutlembz  12400  eucalglt  12454  qredeq  12493  qredeu  12494  divgcdcoprm0  12498  divgcdcoprmex  12499  cncongr1  12500  cncongr2  12501  qnumdenbi  12589  hashgcdlem  12635  coprimeprodsq2  12656  pythagtriplem18  12679  pythagtriplem19  12680  pceu  12693  pcval  12694  pczpre  12695  pcdiv  12700  dvdsprmpweq  12733  dvdsprmpweqnn  12734  difsqpwdvds  12736  pcmpt  12741  pcfac  12748  oddprmdvds  12752  4sqlem2  12787  4sqlem3  12788  4sqlem4  12790  4sqlem12  12800  evenennn  12839  ennnfonelemim  12870  ptex  13171  intopsn  13274  igsumvalx  13296  gsumfzval  13298  gsumpropd  13299  gsumpropd2  13300  gsumress  13302  gsumval2  13304  ismnddef  13325  sgrpidmndm  13327  mndpfo  13345  mhmex  13369  grpid  13446  grpidrcan  13472  grpidlcan  13473  grplactcnv  13509  isghm  13654  f1ghm0to0  13683  conjghm  13687  srgpcomp  13827  ringadd2  13864  rrgval  14099  opprdomnbg  14111  islmod  14128  lss1d  14220  rspsn  14371  expghmap  14444  zndvds0  14487  znf1o  14488  mplvalcoe  14527  istopon  14560  eltg3  14604  restsn  14727  txuni2  14803  txopn  14812  upxp  14819  uptx  14821  txrest  14823  hmeoimaf1o  14861  xmettxlem  15056  xmettx  15057  elply2  15282  elplyr  15287  dvdsppwf1o  15536  mpodvdsmulf1o  15537  perfectlem2  15547  perfect  15548  lgslem1  15552  lgsdirnn0  15599  lgsdinn0  15600  gausslemma2dlem0i  15609  gausslemma2dlem1a  15610  gausslemma2d  15621  lgseisenlem2  15623  lgsquadlem2  15630  2lgslem1b  15641  2lgslem3a1  15649  2lgslem3b1  15650  2lgslem3c1  15651  2lgslem3d1  15652  2lgsoddprmlem2  15658  2sqlem2  15667  2sqlem8  15675  2sqlem9  15676  incistruhgr  15761  upgrex  15774  bj-nn0suc0  16024  bj-inf2vnlem1  16044  bj-nn0sucALT  16052  pwle2  16076  iooref1o  16114