Theorem eqeq2d 2250

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtrd  2271  eq2tri  2298  rspcedeq2vd  2940  rspceeqv  2948  sbceq1g  3167  ifeqeqxdc  3687  euabsn  3781  absneu  3783  ifpprsnssdc  3820  preq12bg  3898  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  mpteq12f  4211  cbvmptf  4225  cbvmpt  4226  exmidsssn  4339  exmidsssnc  4340  opth  4377  eqvinop  4383  moop2  4392  euotd  4395  eusvnf  4599  reusv3i  4605  nlimsucg  4713  nn0suc  4751  opelxp  4804  elvvv  4838  relop  4930  elrnmpt1s  5032  elrnmpt1  5033  elsnres  5100  elxp4  5275  elxp5  5276  relresfld  5317  iotajust  5336  iota1  5352  iota2df  5363  funopg  5411  funcnvuni  5450  fun11iun  5660  funcocnv2  5664  nfvres  5732  ssimaex  5764  fvmptg  5781  fvmptdf  5793  fvopab6  5805  fnmptfvd  5813  fmptco  5874  fsng  5881  fsn2g  5883  funopsn  5891  dfimafnf  5955  foco2  5959  elabrex  5963  elabrexg  5964  abrexco  5965  f1veqaeq  5975  dff13f  5976  f1ocnvfv  5985  f1ocnvfvb  5986  fcofo  5990  fliftfun  6002  fliftval  6006  f1oiso2  6033  riotaeqimp  6063  riota5f  6065  oprabid  6117  rspceov  6128  dfoprab2  6135  mpoeq123dva  6149  mpoeq3dva  6152  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvmpox  6166  mpomptx  6179  ovmpos  6212  ovmpodf  6220  ovmpodv2  6222  ovi3  6226  ov6g  6227  fnrnov  6235  foov  6236  caovcang  6251  caovcan  6254  f1opw2  6296  opabex3d  6350  opabex3  6351  fo1st  6391  fo2nd  6392  elxp6  6403  op1steq  6413  dfoprab4f  6427  fmpox  6436  fnmpoovd  6451  df1st2  6455  df2nd2  6456  xporderlem  6467  cnvoprab  6470  f1od2  6471  brtpos2  6522  dftpos4  6534  tposfn2  6537  recseq  6577  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecabcl  6670  frecsuc  6678  nna0r  6751  eqerlem  6838  qseq2  6858  ecelqsg  6862  snec  6870  qsinxp  6885  ecoptocl  6896  eroveu  6900  th3qlem1  6911  th3qlem2  6912  th3q  6914  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1  7086  mapsnend  7099  mapsnen  7100  en2  7112  xpsnen  7119  xpassen  7128  pw2f1odclem  7134  xpf1o  7144  mapen  7146  mapxpen  7148  mapunen  7151  fidifsnen  7172  ac6sfi  7202  undifdc  7231  djuf1olem  7394  djur  7410  updjud  7423  omp1eomlem  7435  0ct  7448  enumctlemm  7455  fodjuomnilemdc  7485  fodjuomni  7490  fodjumkv  7501  nninfwlporlemd  7513  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  cc2lem  7633  dfplpq2  7722  dfmpq2  7723  enqbreq2  7725  enq0sym  7800  enq0ref  7801  enq0tr  7802  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  mulnnnq0  7818  nqnq0a  7822  nqnq0m  7823  nq0a0  7825  prarloclemcalc  7870  genipv  7877  genpassl  7892  genpassu  7893  addcomprg  7946  mulcomprg  7948  distrlem1prl  7950  distrlem1pru  7951  distrlem5prl  7954  distrlem5pru  7955  1idprl  7958  1idpru  7959  recexprlem1ssl  8001  recexprlem1ssu  8002  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  elreal  8196  axcnre  8249  axcaucvglemval  8265  negeu  8519  subeq0  8554  apreap  8918  apreim  8934  divmulap3  9010  diveqap0  9015  diveqap1  9038  nn0ind-raph  9768  elq  10032  zq  10036  elpq  10060  cnref1o  10062  iccf1o  10418  fzen  10458  fseq1m1p1  10513  fzm1  10518  modqmuladd  10818  modqmuladdnn0  10820  modfzo0difsn  10847  nn0ennn  10885  seqf1oglem1  10971  seq3id2  10978  qsqeqor  11102  bcval5  11217  fihashen1  11254  hashf1lem1  11301  wrdl1exs1  11413  wrdl1s1  11414  wrd2ind  11511  swrdccatin2d  11532  reuccatpfxs1lem  11534  shftlem  11597  shftfvalg  11599  shftfval  11602  negfi  12011  xrmaxiflemcom  12034  xrnegiso  12047  xrnegcon1d  12049  sumeq2  12144  summodc  12169  fsum3  12173  fsum2dlemstep  12220  isumsplit  12277  mertenslemub  12320  mertensabs  12323  prodeq2w  12342  prodeq2  12343  prodmodc  12364  fprodseq  12369  fprod2dlemstep  12408  moddvds  12585  modm1div  12586  dvdsnegb  12594  dvdsabseq  12633  dvdsmod  12648  odd2np1lem  12658  odd2np1  12659  opeo  12683  omeo  12684  divalglemnn  12704  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  bitsinv1lem  12747  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  bezoutlemex  12797  bezoutlemaz  12799  bezoutlembz  12800  eucalglt  12854  qredeq  12893  qredeu  12894  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  qnumdenbi  12991  nn0sqdcq  13007  hashgcdlem  13039  coprimeprodsq2  13060  pythagtriplem18  13083  pythagtriplem19  13084  pceu  13097  pcval  13098  pczpre  13099  pcdiv  13104  dvdsprmpweq  13137  dvdsprmpweqnn  13138  difsqpwdvds  13140  pcmpt  13145  pcfac  13152  oddprmdvds  13156  4sqlem2  13191  4sqlem3  13192  4sqlem4  13194  4sqlem12  13204  ballotfilemfc0  13284  ballotfilemfcc  13285  evenennn  13336  ennnfonelemim  13367  ptex  13671  intopsn  13740  gzsumvalx  13762  gzsumfzval  13764  gzsumress  13765  gzsumval2  13767  ismnddef  13784  sgrpidmndm  13786  mndpfo  13804  mhmex  13822  grpid  13897  grpidrcan  13923  grpidlcan  13924  grplactcnv  13960  isghm  14099  f1ghm0to0  14128  conjghm  14132  gsumvalfi  14236  srgpcomp  14378  ringadd2  14416  rrgval  14654  opprdomnbg  14667  islmod  14711  lss1d  14804  rspsn  14955  expghmap  15026  zndvds0  15069  znf1o  15070  psrbagconf1o  15149  mplvalcoe  15172  istopon  15205  eltg3  15249  restsn  15372  txuni2  15448  txopn  15457  upxp  15464  uptx  15466  txrest  15468  hmeoimaf1o  15506  xmettxlem  15701  xmettx  15702  elply2  15927  elplyr  15932  zprmlogbaplem3  16178  dvdsppwf1o  16244  mpodvdsmulf1o  16245  perfectlem2  16261  perfect  16262  lgslem1  16285  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  gausslemma2d  16354  lgseisenlem2  16356  lgsquadlem2  16363  2lgslem1b  16374  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  2lgsoddprmlem2  16391  2sqlem2  16400  2sqlem8  16408  2sqlem9  16409  incistruhgr  16497  upgrex  16510  usgredg4  16622  usgredgreu  16623  uspgredg2vtxeu  16625  uspgredg2v  16628  usgredg2vlem2  16630  usgredg2v  16631  vtxdgfifival  16698  vtxdumgrfival  16705  1loopgrvd2fi  16712  wlk1walkdom  16766  upgriswlkdc  16767  eupth2lem3lem3fi  16877  eupth2fi  16886  bj-nn0suc0  17142  bj-inf2vnlem1  17162  bj-nn0sucALT  17170  pwle2  17194  iooref1o  17249  qdiff  17265