Theorem eqeq1d 2238

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqeq1d	⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq1 2236	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  rspcedeq1vd  2916  sbceq2g  3146  csbhypf  3163  csbiebt  3164  csbiebg  3167  dfss4st  3437  disjssun  3555  sneqrg  3840  preq12b  3848  preq12bg  3851  disji2  4075  invdisjrab  4077  iin0r  4253  opthg  4324  opeqsn  4339  unisucg  4505  opthreg  4648  tfisi  4679  dmsnopg  5200  relcoi1  5260  iotaeq  5287  iotabi  5288  fneq1  5409  fnun  5429  fnresdisj  5433  fnimadisj  5444  fnimaeq0  5445  sbcfng  5471  foeq1  5546  foco  5561  fveqeq2d  5637  fvelimab  5692  fvun1  5702  fvmptdv2  5726  fneqeql  5745  dffo3  5784  fvsng  5839  fconstfvm  5861  eufnfv  5874  f1veqaeq  5899  dff13f  5900  f1elima  5903  foeqcnvco  5920  f1eqcocnv  5921  acexmidlemab  6001  ovanraleqv  6031  eloprabga  6097  ovmpodv2  6144  ovi3  6148  ovelimab  6162  caovcang  6173  caovcan  6176  caovimo  6205  suppssfv  6220  suppssov1  6221  caofinvl  6250  caofid1  6253  caofid2  6254  uchoice  6289  op1stg  6302  op2ndg  6303  eqop  6329  reldm  6338  xporderlem  6383  tposfo2  6419  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnm0r  6633  nnmord  6671  nnaordex  6682  nnawordex  6683  ereq1  6695  eqerlem  6719  mapsn  6845  endisj  6991  pw2f1odclem  7003  xpf1o  7013  mapxpen  7017  fidifsnen  7040  supelti  7180  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  omp1eomlem  7272  difinfsnlem  7277  nnnninfeq  7306  enomnilem  7316  finomni  7318  exmidomni  7320  fodjuomnilemres  7326  fodjuomni  7327  ismkvnex  7333  mkvprop  7336  fodjumkvlemres  7337  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlporlem  7351  nninfwlpoimlemginf  7354  pm54.43  7374  exmidfodomrlemrALT  7392  cc2lem  7463  addnidpig  7534  ltexpi  7535  dfplpq2  7552  dfmpq2  7553  recexnq  7588  recmulnqg  7589  ltexnqq  7606  halfnqq  7608  enq0tr  7632  nqnq0pi  7636  addnnnq0  7647  addlocpr  7734  ltexprlemru  7810  ltexpri  7811  lteupri  7815  prplnqu  7818  recexpr  7836  addsrpr  7943  mulsrpr  7944  00sr  7967  negexsr  7970  recexgt0sr  7971  srpospr  7981  prsrriota  7986  caucvgsrlemfv  7989  map2psrprg  8003  elrealeu  8027  axrnegex  8077  axprecex  8078  rereceu  8087  recriota  8088  nntopi  8092  axcaucvglemval  8095  axcaucvglemcau  8096  cnegexlem1  8332  cnegex  8335  cnegex2  8336  subval  8349  subadd  8360  subadd2  8361  subsub23  8362  addsubeq4  8372  subcan2  8382  negcon1  8409  subcan  8412  addrsub  8528  ltadd2  8577  ltordlem  8640  recexre  8736  recexap  8811  muleqadd  8826  receuap  8827  divvalap  8832  divmulap  8833  rec11ap  8868  rerecapb  9001  zdiv  9546  uzin  9767  xaddval  10053  xnn0xadd0  10075  xnegdi  10076  xltadd1  10084  icc0r  10134  fznlem  10249  fseq1m1p1  10303  1fv  10347  fzon  10375  fvinim0ffz  10459  ioo0  10491  ico0  10493  ioc0  10494  flqbi  10522  divfl0  10528  modq0  10563  modqmuladdnn0  10602  addmodlteq  10632  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seq3f1olemstep  10748  seq3f1olemp  10749  seq3id  10759  seq3z  10762  qsqeqor  10884  ccat0  11144  wrdl1s1  11178  ccatws1lenp1bg  11183  pfxsuff1eqwrdeq  11246  swrdccatin2  11276  pfxccatin12lem2  11278  mulreap  11390  rennim  11528  resqrexlemex  11551  rsqrmo  11553  resqrtcl  11555  rersqrtthlem  11556  sqrtsq2  11569  isumss  11917  fsum00  11988  telfsumo  11992  pwm1geoserap1  12034  prodssdc  12115  absefib  12297  efieq1re  12298  divides  12315  dvdsval2  12316  nndivides  12323  dvds0lem  12327  dvds1lem  12328  dvds2lem  12329  negdvdsb  12333  muldvds1  12342  muldvds2  12343  dvdscmulr  12346  dvdsmulcr  12347  dvdstr  12354  dvdsabseq  12373  divconjdvds  12375  odd2np1lem  12398  odd2np1  12399  even2n  12400  oddm1even  12401  2tp1odd  12410  opeo  12423  omeo  12424  m1exp1  12427  divalgb  12451  gcdaddm  12520  gcdabs1  12525  bezout  12547  gcdmultiple  12556  gcdmultiplez  12557  rplpwr  12563  rppwr  12564  nninfctlemfo  12576  alginv  12584  algcvga  12588  algfx  12589  eucalgval2  12590  coprmdvds  12629  qredeq  12633  qredeu  12634  divgcdcoprm0  12638  divgcdcoprmex  12639  cncongr1  12640  rpexp  12690  rpexp12i  12692  cncongrprm  12694  qnumdenbi  12729  phival  12750  phicl2  12751  dfphi2  12757  phiprmpw  12759  phimullem  12762  eulerthlem1  12764  eulerthlemfi  12765  eulerthlemrprm  12766  eulerthlemth  12769  eulerth  12770  fermltl  12771  hashgcdlem  12775  phisum  12778  odzval  12779  odzdvds  12783  reumodprminv  12791  modprm0  12792  nnnn0modprm0  12793  modprmn0modprm0  12794  coprimeprodsq  12795  coprimeprodsq2  12796  pythagtriplem2  12804  pythagtrip  12821  pceulem  12832  pcval  12834  pcqmul  12841  pcqcl  12844  pcabs  12864  pc2dvds  12868  pcaddlem  12877  pcadd  12878  pcmpt  12881  prmpwdvds  12893  pockthi  12896  4sqlem12  12940  ennnfonelemhf1o  12999  fvprif  13391  mgmidmo  13420  grpidvalg  13421  grpidpropdg  13422  ismgmid  13425  ismgmid2  13428  mgmidsssn0  13432  grpinvalem  13433  grprida  13435  igsumvalx  13437  gsumress  13443  ismnddef  13466  sgrpidmndm  13468  ismndd  13485  mndpropd  13488  mndinvmod  13493  mnd1  13503  ismhm  13509  gsumvallem2  13541  grpinvex  13558  isgrpd2  13569  isgrpd  13571  dfgrp2  13575  grpinveu  13586  grpinvval  13591  grplinv  13598  isgrpinv  13602  grplrinv  13605  grpidinv2  13606  grpidinv  13607  grplmulf1o  13622  grpsubeq0  13634  grpsubadd  13636  dfgrp3mlem  13646  dfgrp3m  13647  grp1  13654  imasgrp2  13662  qusgrp2  13665  mhmmnd  13668  ghmgrp  13670  mulgval  13674  mulgaddcom  13698  eqg0el  13781  ghmeqker  13823  ghmf1  13825  conjnmzb  13832  ablsubadd  13864  ablsubsub23  13877  rngmneg1  13925  rngmneg2  13926  dfur2g  13940  srgideu  13950  srgidmlem  13956  issrgid  13959  srgrz  13962  srglz  13963  srgisid  13964  srg1zr  13965  ringideu  13995  ringidmlem  14000  isringid  14003  ringid  14004  qusring2  14044  oppr0g  14059  oppr1g  14060  dvdsrvald  14072  dvdsrmuld  14075  dvdsr01  14083  dvdsr02  14084  opprunitd  14089  crngunit  14090  unitinvinv  14103  dvreq1  14121  dvdsrpropdg  14126  rhmdvdsr  14154  lringuplu  14175  subrg1  14210  subrgdvds  14214  isrrg  14242  rrgeq0i  14243  rrgeq0  14244  domneq0  14251  islmod  14270  islmodd  14272  lmodprop2d  14327  lss1d  14362  cnfldui  14568  znval  14615  znidom  14636  znunit  14638  znrrg  14639  mplelbascoe  14671  ntreq0  14821  ispsmet  15012  psmet0  15016  ismet  15033  isxmet  15034  xmeteq0  15048  metn0  15067  xmetres2  15068  xblss2ps  15093  xblss2  15094  xmseq0  15157  comet  15188  bdxmet  15190  cnmet  15219  ivthdec  15333  ivthreinc  15334  elply2  15424  reeff1o  15462  ioocosf1o  15543  logbgcd1irr  15656  logbgcd1irraplemexp  15657  mpodvdsmulf1o  15679  lgsval  15698  lgsdir  15729  lgsne0  15732  lgsprme0  15736  lgsdirnn0  15741  gausslemma2dlem0c  15745  gausslemma2dlem0i  15751  gausslemma2dlem7  15762  gausslemma2d  15763  lgseisenlem2  15765  lgseisenlem3  15766  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem2  15776  lgsquad3  15778  m1lgs  15779  2lgs  15798  2sqlem7  15815  2sqlem8  15817  2sqlem9  15818  edg0iedg0g  15881  upgredg  15957  ushgredgedgloop  16041  vtxdgfval  16047  vtxdgop  16051  vtxdeqd  16055  vtxdfifiun  16056  wksfval  16063  wlklenvclwlk  16114  bj-charfunbi  16229  2omap  16418  pw1map  16420  pwle2  16423  subctctexmid  16425  peano4nninf  16432  nninfalllem1  16434  nninfsellemdc  16436  nninfsellemeq  16440  nninfsellemqall  16441  nninfsellemeqinf  16442  isomninnlem  16458  trilpolemlt1  16469  trirec0  16472  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480  dceqnconst  16488  dcapnconst  16489