Theorem eqeq2d 2187

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 2185	. 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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  eqtrd  2208  eq2tri  2235  rspcedeq2vd  2849  rspceeqv  2857  sbceq1g  3075  euabsn  3659  absneu  3661  preq12bg  3769  cbvopab  4069  cbvopab1  4071  cbvopab2  4072  cbvopab1s  4073  cbvopab2v  4075  mpteq12f  4078  cbvmptf  4092  cbvmpt  4093  exmidsssn  4197  exmidsssnc  4198  opth  4231  eqvinop  4237  moop2  4245  euotd  4248  eusvnf  4447  reusv3i  4453  nlimsucg  4559  nn0suc  4597  opelxp  4650  elvvv  4683  relop  4770  elrnmpt1s  4870  elrnmpt1  4871  elsnres  4937  elxp4  5108  elxp5  5109  relresfld  5150  iotajust  5169  iota1  5184  iota2df  5194  funopg  5242  funcnvuni  5277  fun11iun  5474  funcocnv2  5478  nfvres  5540  ssimaex  5569  fvmptg  5584  fvmptdf  5595  fvopab6  5604  fnmptfvd  5612  fmptco  5674  fsng  5681  foco2  5745  elabrex  5749  abrexco  5750  f1veqaeq  5760  dff13f  5761  f1ocnvfv  5770  f1ocnvfvb  5771  fcofo  5775  fliftfun  5787  fliftval  5791  f1oiso2  5818  riota5f  5845  oprabid  5897  rspceov  5907  dfoprab2  5912  mpoeq123dva  5926  mpoeq3dva  5929  cbvoprab1  5937  cbvoprab2  5938  cbvoprab12  5939  cbvmpox  5943  mpomptx  5956  ovmpos  5988  ovmpodf  5996  ovmpodv2  5998  ovi3  6001  ov6g  6002  fnrnov  6010  foov  6011  caovcang  6026  caovcan  6029  f1opw2  6067  opabex3d  6112  opabex3  6113  fo1st  6148  fo2nd  6149  elxp6  6160  op1steq  6170  dfoprab4f  6184  fmpox  6191  fnmpoovd  6206  df1st2  6210  df2nd2  6211  xporderlem  6222  cnvoprab  6225  f1od2  6226  brtpos2  6242  dftpos4  6254  tposfn2  6257  recseq  6297  tfr1onlemaccex  6339  tfrcllemaccex  6352  frecabcl  6390  frecsuc  6398  nna0r  6469  eqerlem  6556  qseq2  6574  ecelqsg  6578  snec  6586  qsinxp  6601  ecoptocl  6612  eroveu  6616  th3qlem1  6627  th3qlem2  6628  th3q  6630  mapsncnv  6685  elixpsn  6725  ixpsnf1o  6726  en1  6789  mapsnen  6801  xpsnen  6811  xpassen  6820  xpf1o  6834  mapen  6836  mapxpen  6838  fidifsnen  6860  ac6sfi  6888  undifdc  6913  djuf1olem  7042  djur  7058  updjud  7071  omp1eomlem  7083  0ct  7096  enumctlemm  7103  fodjuomnilemdc  7132  fodjuomni  7137  fodjumkv  7148  nninfwlporlemd  7160  exmidfodomrlemeldju  7188  exmidfodomrlemreseldju  7189  cc2lem  7240  dfplpq2  7328  dfmpq2  7329  enqbreq2  7331  enq0sym  7406  enq0ref  7407  enq0tr  7408  addnq0mo  7421  mulnq0mo  7422  addnnnq0  7423  mulnnnq0  7424  nqnq0a  7428  nqnq0m  7429  nq0a0  7431  prarloclemcalc  7476  genipv  7483  genpassl  7498  genpassu  7499  addcomprg  7552  mulcomprg  7554  distrlem1prl  7556  distrlem1pru  7557  distrlem5prl  7560  distrlem5pru  7561  1idprl  7564  1idpru  7565  recexprlem1ssl  7607  recexprlem1ssu  7608  addsrmo  7717  mulsrmo  7718  addsrpr  7719  mulsrpr  7720  elreal  7802  axcnre  7855  axcaucvglemval  7871  negeu  8122  subeq0  8157  apreap  8518  apreim  8534  divmulap3  8606  diveqap0  8611  diveqap1  8634  nn0ind-raph  9341  elq  9593  zq  9597  elpq  9619  cnref1o  9621  iccf1o  9973  fzen  10011  fseq1m1p1  10063  fzm1  10068  modqmuladd  10334  modqmuladdnn0  10336  modfzo0difsn  10363  nn0ennn  10401  seq3id2  10477  qsqeqor  10598  bcval5  10709  fihashen1  10745  shftlem  10791  shftfvalg  10793  shftfval  10796  negfi  11202  xrmaxiflemcom  11223  xrnegiso  11236  xrnegcon1d  11238  sumeq2  11333  summodc  11357  fsum3  11361  fsum2dlemstep  11408  isumsplit  11465  mertenslemub  11508  mertensabs  11511  prodeq2w  11530  prodeq2  11531  prodmodc  11552  fprodseq  11557  fprod2dlemstep  11596  moddvds  11772  modm1div  11773  dvdsnegb  11781  dvdsabseq  11818  dvdsmod  11833  odd2np1lem  11842  odd2np1  11843  opeo  11867  omeo  11868  divalglemnn  11888  divalglemeunn  11891  divalglemex  11892  divalglemeuneg  11893  bezoutlemnewy  11962  bezoutlema  11965  bezoutlemb  11966  bezoutlemex  11967  bezoutlemaz  11969  bezoutlembz  11970  eucalglt  12022  qredeq  12061  qredeu  12062  divgcdcoprm0  12066  divgcdcoprmex  12067  cncongr1  12068  cncongr2  12069  qnumdenbi  12157  hashgcdlem  12203  coprimeprodsq2  12223  pythagtriplem18  12246  pythagtriplem19  12247  pceu  12260  pcval  12261  pczpre  12262  pcdiv  12267  dvdsprmpweq  12299  dvdsprmpweqnn  12300  difsqpwdvds  12302  pcmpt  12306  pcfac  12313  oddprmdvds  12317  4sqlem2  12352  4sqlem3  12353  4sqlem4  12355  evenennn  12359  ennnfonelemim  12390  intopsn  12650  ismnddef  12683  sgrpidmndm  12685  mndpfo  12703  grpid  12772  grpidrcan  12794  grpidlcan  12795  grplactcnv  12831  srgpcomp  12966  ringadd2  13003  istopon  13062  eltg3  13108  restsn  13231  txuni2  13307  txopn  13316  upxp  13323  uptx  13325  txrest  13327  hmeoimaf1o  13365  xmettxlem  13560  xmettx  13561  lgslem1  13952  lgsdirnn0  13999  lgsdinn0  14000  2sqlem2  14002  2sqlem8  14010  2sqlem9  14011  bj-nn0suc0  14242  bj-inf2vnlem1  14262  bj-nn0sucALT  14270  pwle2  14288  iooref1o  14323