Theorem eqeq2d 2189

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtrd  2210  eq2tri  2237  rspcedeq2vd  2853  rspceeqv  2861  sbceq1g  3079  euabsn  3664  absneu  3666  preq12bg  3775  cbvopab  4076  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  cbvopab2v  4082  mpteq12f  4085  cbvmptf  4099  cbvmpt  4100  exmidsssn  4204  exmidsssnc  4205  opth  4239  eqvinop  4245  moop2  4253  euotd  4256  eusvnf  4455  reusv3i  4461  nlimsucg  4567  nn0suc  4605  opelxp  4658  elvvv  4691  relop  4779  elrnmpt1s  4879  elrnmpt1  4880  elsnres  4946  elxp4  5118  elxp5  5119  relresfld  5160  iotajust  5179  iota1  5194  iota2df  5204  funopg  5252  funcnvuni  5287  fun11iun  5484  funcocnv2  5488  nfvres  5550  ssimaex  5579  fvmptg  5594  fvmptdf  5605  fvopab6  5614  fnmptfvd  5622  fmptco  5684  fsng  5691  foco2  5756  elabrex  5760  elabrexg  5761  abrexco  5762  f1veqaeq  5772  dff13f  5773  f1ocnvfv  5782  f1ocnvfvb  5783  fcofo  5787  fliftfun  5799  fliftval  5803  f1oiso2  5830  riota5f  5857  oprabid  5909  rspceov  5919  dfoprab2  5924  mpoeq123dva  5938  mpoeq3dva  5941  cbvoprab1  5949  cbvoprab2  5950  cbvoprab12  5951  cbvmpox  5955  mpomptx  5968  ovmpos  6000  ovmpodf  6008  ovmpodv2  6010  ovi3  6013  ov6g  6014  fnrnov  6022  foov  6023  caovcang  6038  caovcan  6041  f1opw2  6079  opabex3d  6124  opabex3  6125  fo1st  6160  fo2nd  6161  elxp6  6172  op1steq  6182  dfoprab4f  6196  fmpox  6203  fnmpoovd  6218  df1st2  6222  df2nd2  6223  xporderlem  6234  cnvoprab  6237  f1od2  6238  brtpos2  6254  dftpos4  6266  tposfn2  6269  recseq  6309  tfr1onlemaccex  6351  tfrcllemaccex  6364  frecabcl  6402  frecsuc  6410  nna0r  6481  eqerlem  6568  qseq2  6586  ecelqsg  6590  snec  6598  qsinxp  6613  ecoptocl  6624  eroveu  6628  th3qlem1  6639  th3qlem2  6640  th3q  6642  mapsncnv  6697  elixpsn  6737  ixpsnf1o  6738  en1  6801  mapsnen  6813  xpsnen  6823  xpassen  6832  xpf1o  6846  mapen  6848  mapxpen  6850  fidifsnen  6872  ac6sfi  6900  undifdc  6925  djuf1olem  7054  djur  7070  updjud  7083  omp1eomlem  7095  0ct  7108  enumctlemm  7115  fodjuomnilemdc  7144  fodjuomni  7149  fodjumkv  7160  nninfwlporlemd  7172  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  cc2lem  7267  dfplpq2  7355  dfmpq2  7356  enqbreq2  7358  enq0sym  7433  enq0ref  7434  enq0tr  7435  addnq0mo  7448  mulnq0mo  7449  addnnnq0  7450  mulnnnq0  7451  nqnq0a  7455  nqnq0m  7456  nq0a0  7458  prarloclemcalc  7503  genipv  7510  genpassl  7525  genpassu  7526  addcomprg  7579  mulcomprg  7581  distrlem1prl  7583  distrlem1pru  7584  distrlem5prl  7587  distrlem5pru  7588  1idprl  7591  1idpru  7592  recexprlem1ssl  7634  recexprlem1ssu  7635  addsrmo  7744  mulsrmo  7745  addsrpr  7746  mulsrpr  7747  elreal  7829  axcnre  7882  axcaucvglemval  7898  negeu  8150  subeq0  8185  apreap  8546  apreim  8562  divmulap3  8636  diveqap0  8641  diveqap1  8664  nn0ind-raph  9372  elq  9624  zq  9628  elpq  9650  cnref1o  9652  iccf1o  10006  fzen  10045  fseq1m1p1  10097  fzm1  10102  modqmuladd  10368  modqmuladdnn0  10370  modfzo0difsn  10397  nn0ennn  10435  seq3id2  10511  qsqeqor  10633  bcval5  10745  fihashen1  10781  shftlem  10827  shftfvalg  10829  shftfval  10832  negfi  11238  xrmaxiflemcom  11259  xrnegiso  11272  xrnegcon1d  11274  sumeq2  11369  summodc  11393  fsum3  11397  fsum2dlemstep  11444  isumsplit  11501  mertenslemub  11544  mertensabs  11547  prodeq2w  11566  prodeq2  11567  prodmodc  11588  fprodseq  11593  fprod2dlemstep  11632  moddvds  11808  modm1div  11809  dvdsnegb  11817  dvdsabseq  11855  dvdsmod  11870  odd2np1lem  11879  odd2np1  11880  opeo  11904  omeo  11905  divalglemnn  11925  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  bezoutlemnewy  11999  bezoutlema  12002  bezoutlemb  12003  bezoutlemex  12004  bezoutlemaz  12006  bezoutlembz  12007  eucalglt  12059  qredeq  12098  qredeu  12099  divgcdcoprm0  12103  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  qnumdenbi  12194  hashgcdlem  12240  coprimeprodsq2  12260  pythagtriplem18  12283  pythagtriplem19  12284  pceu  12297  pcval  12298  pczpre  12299  pcdiv  12304  dvdsprmpweq  12336  dvdsprmpweqnn  12337  difsqpwdvds  12339  pcmpt  12343  pcfac  12350  oddprmdvds  12354  4sqlem2  12389  4sqlem3  12390  4sqlem4  12392  evenennn  12396  ennnfonelemim  12427  ptex  12718  intopsn  12791  ismnddef  12824  sgrpidmndm  12826  mndpfo  12844  grpid  12917  grpidrcan  12940  grpidlcan  12941  grplactcnv  12977  srgpcomp  13178  ringadd2  13215  islmod  13386  lss1d  13475  istopon  13552  eltg3  13596  restsn  13719  txuni2  13795  txopn  13804  upxp  13811  uptx  13813  txrest  13815  hmeoimaf1o  13853  xmettxlem  14048  xmettx  14049  lgslem1  14440  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem2  14490  2lgsoddprmlem2  14493  2sqlem2  14501  2sqlem8  14509  2sqlem9  14510  bj-nn0suc0  14741  bj-inf2vnlem1  14761  bj-nn0sucALT  14769  pwle2  14787  iooref1o  14821