Theorem eqeq2d 2205

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtrd  2226  eq2tri  2253  rspcedeq2vd  2874  rspceeqv  2882  sbceq1g  3100  euabsn  3688  absneu  3690  preq12bg  3799  cbvopab  4100  cbvopab1  4102  cbvopab2  4103  cbvopab1s  4104  cbvopab2v  4106  mpteq12f  4109  cbvmptf  4123  cbvmpt  4124  exmidsssn  4231  exmidsssnc  4232  opth  4266  eqvinop  4272  moop2  4280  euotd  4283  eusvnf  4484  reusv3i  4490  nlimsucg  4598  nn0suc  4636  opelxp  4689  elvvv  4722  relop  4812  elrnmpt1s  4912  elrnmpt1  4913  elsnres  4979  elxp4  5153  elxp5  5154  relresfld  5195  iotajust  5214  iota1  5229  iota2df  5240  funopg  5288  funcnvuni  5323  fun11iun  5521  funcocnv2  5525  nfvres  5588  ssimaex  5618  fvmptg  5633  fvmptdf  5645  fvopab6  5654  fnmptfvd  5662  fmptco  5724  fsng  5731  foco2  5796  elabrex  5800  elabrexg  5801  abrexco  5802  f1veqaeq  5812  dff13f  5813  f1ocnvfv  5822  f1ocnvfvb  5823  fcofo  5827  fliftfun  5839  fliftval  5843  f1oiso2  5870  riota5f  5898  oprabid  5950  rspceov  5960  dfoprab2  5965  mpoeq123dva  5979  mpoeq3dva  5982  cbvoprab1  5990  cbvoprab2  5991  cbvoprab12  5992  cbvmpox  5996  mpomptx  6009  ovmpos  6042  ovmpodf  6050  ovmpodv2  6052  ovi3  6055  ov6g  6056  fnrnov  6064  foov  6065  caovcang  6080  caovcan  6083  f1opw2  6124  opabex3d  6173  opabex3  6174  fo1st  6210  fo2nd  6211  elxp6  6222  op1steq  6232  dfoprab4f  6246  fmpox  6253  fnmpoovd  6268  df1st2  6272  df2nd2  6273  xporderlem  6284  cnvoprab  6287  f1od2  6288  brtpos2  6304  dftpos4  6316  tposfn2  6319  recseq  6359  tfr1onlemaccex  6401  tfrcllemaccex  6414  frecabcl  6452  frecsuc  6460  nna0r  6531  eqerlem  6618  qseq2  6638  ecelqsg  6642  snec  6650  qsinxp  6665  ecoptocl  6676  eroveu  6680  th3qlem1  6691  th3qlem2  6692  th3q  6694  mapsncnv  6749  elixpsn  6789  ixpsnf1o  6790  en1  6853  mapsnen  6865  xpsnen  6875  xpassen  6884  pw2f1odclem  6890  xpf1o  6900  mapen  6902  mapxpen  6904  fidifsnen  6926  ac6sfi  6954  undifdc  6980  djuf1olem  7112  djur  7128  updjud  7141  omp1eomlem  7153  0ct  7166  enumctlemm  7173  fodjuomnilemdc  7203  fodjuomni  7208  fodjumkv  7219  nninfwlporlemd  7231  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  cc2lem  7326  dfplpq2  7414  dfmpq2  7415  enqbreq2  7417  enq0sym  7492  enq0ref  7493  enq0tr  7494  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  mulnnnq0  7510  nqnq0a  7514  nqnq0m  7515  nq0a0  7517  prarloclemcalc  7562  genipv  7569  genpassl  7584  genpassu  7585  addcomprg  7638  mulcomprg  7640  distrlem1prl  7642  distrlem1pru  7643  distrlem5prl  7646  distrlem5pru  7647  1idprl  7650  1idpru  7651  recexprlem1ssl  7693  recexprlem1ssu  7694  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  elreal  7888  axcnre  7941  axcaucvglemval  7957  negeu  8210  subeq0  8245  apreap  8606  apreim  8622  divmulap3  8696  diveqap0  8701  diveqap1  8724  nn0ind-raph  9434  elq  9687  zq  9691  elpq  9714  cnref1o  9716  iccf1o  10070  fzen  10109  fseq1m1p1  10161  fzm1  10166  modqmuladd  10437  modqmuladdnn0  10439  modfzo0difsn  10466  nn0ennn  10504  seqf1oglem1  10590  seq3id2  10597  qsqeqor  10721  bcval5  10834  fihashen1  10870  shftlem  10960  shftfvalg  10962  shftfval  10965  negfi  11371  xrmaxiflemcom  11392  xrnegiso  11405  xrnegcon1d  11407  sumeq2  11502  summodc  11526  fsum3  11530  fsum2dlemstep  11577  isumsplit  11634  mertenslemub  11677  mertensabs  11680  prodeq2w  11699  prodeq2  11700  prodmodc  11721  fprodseq  11726  fprod2dlemstep  11765  moddvds  11942  modm1div  11943  dvdsnegb  11951  dvdsabseq  11989  dvdsmod  12004  odd2np1lem  12013  odd2np1  12014  opeo  12038  omeo  12039  divalglemnn  12059  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  bezoutlemex  12138  bezoutlemaz  12140  bezoutlembz  12141  eucalglt  12195  qredeq  12234  qredeu  12235  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  qnumdenbi  12330  hashgcdlem  12376  coprimeprodsq2  12396  pythagtriplem18  12419  pythagtriplem19  12420  pceu  12433  pcval  12434  pczpre  12435  pcdiv  12440  dvdsprmpweq  12473  dvdsprmpweqnn  12474  difsqpwdvds  12476  pcmpt  12481  pcfac  12488  oddprmdvds  12492  4sqlem2  12527  4sqlem3  12528  4sqlem4  12530  4sqlem12  12540  evenennn  12550  ennnfonelemim  12581  ptex  12875  intopsn  12950  igsumvalx  12972  gsumfzval  12974  gsumpropd  12975  gsumpropd2  12976  gsumress  12978  gsumval2  12980  ismnddef  12999  sgrpidmndm  13001  mndpfo  13019  mhmex  13034  grpid  13111  grpidrcan  13137  grpidlcan  13138  grplactcnv  13174  isghm  13313  f1ghm0to0  13342  conjghm  13346  srgpcomp  13486  ringadd2  13523  rrgval  13758  opprdomnbg  13770  islmod  13787  lss1d  13879  rspsn  14030  expghmap  14095  zndvds0  14138  znf1o  14139  istopon  14181  eltg3  14225  restsn  14348  txuni2  14424  txopn  14433  upxp  14440  uptx  14442  txrest  14444  hmeoimaf1o  14482  xmettxlem  14677  xmettx  14678  elply2  14881  elplyr  14886  lgslem1  15116  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  gausslemma2d  15185  lgseisenlem2  15187  2lgsoddprmlem2  15194  2sqlem2  15202  2sqlem8  15210  2sqlem9  15211  bj-nn0suc0  15442  bj-inf2vnlem1  15462  bj-nn0sucALT  15470  pwle2  15489  iooref1o  15524