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  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab2v  4209  mpteq12f  4212  cbvmptf  4227  cbvmpt  4228  exmidsssn  4341  exmidsssnc  4342  opth  4379  eqvinop  4385  moop2  4394  euotd  4397  eusvnf  4601  reusv3i  4607  nlimsucg  4715  nn0suc  4753  opelxp  4806  elvvv  4840  relop  4932  elrnmpt1s  5034  elrnmpt1  5035  elsnres  5102  elxp4  5278  elxp5  5279  relresfld  5320  iotajust  5339  iota1  5355  iota2df  5366  funopg  5414  funcnvuni  5453  fun11iun  5663  funcocnv2  5667  nfvres  5735  ssimaex  5767  fvmptg  5784  fvmptdf  5796  fvopab6  5808  fnmptfvd  5816  fmptco  5877  fsng  5884  fsn2g  5886  funopsn  5894  dfimafnf  5958  foco2  5962  elabrex  5966  elabrexg  5967  abrexco  5968  f1veqaeq  5978  dff13f  5979  f1ocnvfv  5988  f1ocnvfvb  5989  fcofo  5993  fliftfun  6005  fliftval  6009  f1oiso2  6036  riotaeqimp  6066  riota5f  6068  oprabid  6120  rspceov  6131  dfoprab2  6138  mpoeq123dva  6152  mpoeq3dva  6155  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvmpox  6169  mpomptx  6182  ovmpos  6215  ovmpodf  6223  ovmpodv2  6225  ovi3  6229  ov6g  6230  fnrnov  6238  foov  6239  caovcang  6254  caovcan  6257  f1opw2  6299  opabex3d  6354  opabex3  6355  fo1st  6395  fo2nd  6396  elxp6  6407  op1steq  6417  dfoprab4f  6431  fmpox  6440  fnmpoovd  6455  df1st2  6459  df2nd2  6460  xporderlem  6471  cnvoprab  6474  f1od2  6475  brtpos2  6526  dftpos4  6538  tposfn2  6541  recseq  6581  tfr1onlemaccex  6623  tfrcllemaccex  6636  frecabcl  6674  frecsuc  6682  nna0r  6755  eqerlem  6842  qseq2  6862  ecelqsg  6866  snec  6874  qsinxp  6889  ecoptocl  6900  eroveu  6904  th3qlem1  6915  th3qlem2  6916  th3q  6918  mapsncnv  6981  elixpsn  7021  ixpsnf1o  7022  en1  7090  mapsnend  7103  mapsnen  7104  en2  7116  xpsnen  7123  xpassen  7132  pw2f1odclem  7138  xpf1o  7148  mapen  7150  mapxpen  7152  mapunen  7155  fidifsnen  7176  ac6sfi  7206  undifdc  7235  djuf1olem  7399  djur  7415  updjud  7428  omp1eomlem  7440  0ct  7453  enumctlemm  7460  fodjuomnilemdc  7490  fodjuomni  7495  fodjumkv  7506  nninfwlporlemd  7518  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  cc2lem  7638  dfplpq2  7727  dfmpq2  7728  enqbreq2  7730  enq0sym  7805  enq0ref  7806  enq0tr  7807  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  nqnq0a  7827  nqnq0m  7828  nq0a0  7830  prarloclemcalc  7875  genipv  7882  genpassl  7897  genpassu  7898  addcomprg  7951  mulcomprg  7953  distrlem1prl  7955  distrlem1pru  7956  distrlem5prl  7959  distrlem5pru  7960  1idprl  7963  1idpru  7964  recexprlem1ssl  8006  recexprlem1ssu  8007  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  elreal  8201  axcnre  8254  axcaucvglemval  8270  negeu  8524  subeq0  8559  apreap  8923  apreim  8939  divmulap3  9015  diveqap0  9020  diveqap1  9043  nn0ind-raph  9774  elq  10038  zq  10042  elpq  10066  cnref1o  10068  iccf1o  10424  fzen  10464  fseq1m1p1  10519  fzm1  10524  modqmuladd  10824  modqmuladdnn0  10826  modfzo0difsn  10853  nn0ennn  10891  seqf1oglem1  10977  seq3id2  10984  qsqeqor  11108  bcval5  11223  fihashen1  11260  hashf1lem1  11307  wrdl1exs1  11419  wrdl1s1  11420  wrd2ind  11517  swrdccatin2d  11538  reuccatpfxs1lem  11540  shftlem  11603  shftfvalg  11605  shftfval  11608  negfi  12017  xrmaxiflemcom  12040  xrnegiso  12053  xrnegcon1d  12055  sumeq2  12150  summodc  12175  fsum3  12179  fsum2dlemstep  12226  isumsplit  12283  mertenslemub  12326  mertensabs  12329  prodeq2w  12348  prodeq2  12349  prodmodc  12370  fprodseq  12375  fprod2dlemstep  12414  moddvds  12591  modm1div  12592  dvdsnegb  12600  dvdsabseq  12639  dvdsmod  12654  odd2np1lem  12664  odd2np1  12665  opeo  12689  omeo  12690  divalglemnn  12710  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  bitsinv1lem  12753  bezoutlemnewy  12798  bezoutlema  12801  bezoutlemb  12802  bezoutlemex  12803  bezoutlemaz  12805  bezoutlembz  12806  eucalglt  12860  qredeq  12899  qredeu  12900  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  qnumdenbi  12997  nn0sqdcq  13013  hashgcdlem  13045  coprimeprodsq2  13066  pythagtriplem18  13089  pythagtriplem19  13090  pceu  13103  pcval  13104  pczpre  13105  pcdiv  13110  dvdsprmpweq  13143  dvdsprmpweqnn  13144  difsqpwdvds  13146  pcmpt  13151  pcfac  13158  oddprmdvds  13162  4sqlem2  13197  4sqlem3  13198  4sqlem4  13200  4sqlem12  13210  ballotfilemfc0  13290  ballotfilemfcc  13291  evenennn  13342  ennnfonelemim  13373  ptex  13677  intopsn  13746  gzsumvalx  13768  gzsumfzval  13770  gzsumress  13771  gzsumval2  13773  ismnddef  13790  sgrpidmndm  13792  mndpfo  13810  mhmex  13828  grpid  13903  grpidrcan  13929  grpidlcan  13930  grplactcnv  13966  isghm  14105  f1ghm0to0  14134  conjghm  14138  gsumvalfi  14242  srgpcomp  14401  ringadd2  14439  rrgval  14679  opprdomnbg  14692  islmod  14736  lss1d  14829  rspsn  14980  expghmap  15051  zndvds0  15094  znf1o  15095  psrbagconf1o  15174  mplvalcoe  15206  istopon  15239  eltg3  15283  restsn  15406  txuni2  15482  txopn  15491  upxp  15498  uptx  15500  txrest  15502  hmeoimaf1o  15540  xmettxlem  15735  xmettx  15736  elply2  15961  elplyr  15966  zprmlogbaplem3  16217  dvdsppwf1o  16283  mpodvdsmulf1o  16284  perfectlem2  16300  perfect  16301  lgslem1  16324  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  gausslemma2d  16393  lgseisenlem2  16395  lgsquadlem2  16402  2lgslem1b  16413  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  2lgsoddprmlem2  16430  2sqlem2  16439  2sqlem8  16447  2sqlem9  16448  incistruhgr  16536  upgrex  16549  usgredg4  16661  usgredgreu  16662  uspgredg2vtxeu  16664  uspgredg2v  16667  usgredg2vlem2  16669  usgredg2v  16670  vtxdgfifival  16737  vtxdumgrfival  16744  1loopgrvd2fi  16751  wlk1walkdom  16805  upgriswlkdc  16806  eupth2lem3lem3fi  16916  eupth2fi  16925  bj-nn0suc0  17181  bj-inf2vnlem1  17201  bj-nn0sucALT  17209  pwle2  17233  iooref1o  17289  qdiff  17305