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  2917  sbceq2g  3147  csbhypf  3164  csbiebt  3165  csbiebg  3168  dfss4st  3438  disjssun  3556  sneqrg  3843  preq12b  3851  preq12bg  3854  disji2  4078  invdisjrab  4080  iin0r  4257  opthg  4328  opeqsn  4343  unisucg  4509  opthreg  4652  tfisi  4683  dmsnopg  5206  relcoi1  5266  iotaeq  5293  iotabi  5294  fneq1  5415  fnun  5435  fnresdisj  5439  fnimadisj  5450  fnimaeq0  5451  sbcfng  5477  foeq1  5552  foco  5567  fveqeq2d  5643  fvelimab  5698  fvun1  5708  fvmptdv2  5732  fneqeql  5751  dffo3  5790  fvsng  5845  fconstfvm  5867  eufnfv  5880  f1veqaeq  5905  dff13f  5906  f1elima  5909  foeqcnvco  5926  f1eqcocnv  5927  acexmidlemab  6007  ovanraleqv  6037  eloprabga  6103  ovmpodv2  6150  ovi3  6154  ovelimab  6168  caovcang  6179  caovcan  6182  caovimo  6211  suppssfv  6226  suppssov1  6227  caofinvl  6256  caofid1  6259  caofid2  6260  uchoice  6295  op1stg  6308  op2ndg  6309  eqop  6335  reldm  6344  xporderlem  6391  tposfo2  6428  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  nnm0r  6642  nnmord  6680  nnaordex  6691  nnawordex  6692  ereq1  6704  eqerlem  6728  mapsn  6854  endisj  7003  pw2f1odclem  7015  xpf1o  7025  mapxpen  7029  fidifsnen  7052  supelti  7192  updjudhcoinlf  7270  updjudhcoinrg  7271  updjud  7272  omp1eomlem  7284  difinfsnlem  7289  nnnninfeq  7318  enomnilem  7328  finomni  7330  exmidomni  7332  fodjuomnilemres  7338  fodjuomni  7339  ismkvnex  7345  mkvprop  7348  fodjumkvlemres  7349  enmkvlem  7351  enwomnilem  7359  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemginf  7366  pm54.43  7386  exmidfodomrlemrALT  7404  cc2lem  7475  addnidpig  7546  ltexpi  7547  dfplpq2  7564  dfmpq2  7565  recexnq  7600  recmulnqg  7601  ltexnqq  7618  halfnqq  7620  enq0tr  7644  nqnq0pi  7648  addnnnq0  7659  addlocpr  7746  ltexprlemru  7822  ltexpri  7823  lteupri  7827  prplnqu  7830  recexpr  7848  addsrpr  7955  mulsrpr  7956  00sr  7979  negexsr  7982  recexgt0sr  7983  srpospr  7993  prsrriota  7998  caucvgsrlemfv  8001  map2psrprg  8015  elrealeu  8039  axrnegex  8089  axprecex  8090  rereceu  8099  recriota  8100  nntopi  8104  axcaucvglemval  8107  axcaucvglemcau  8108  cnegexlem1  8344  cnegex  8347  cnegex2  8348  subval  8361  subadd  8372  subadd2  8373  subsub23  8374  addsubeq4  8384  subcan2  8394  negcon1  8421  subcan  8424  addrsub  8540  ltadd2  8589  ltordlem  8652  recexre  8748  recexap  8823  muleqadd  8838  receuap  8839  divvalap  8844  divmulap  8845  rec11ap  8880  rerecapb  9013  zdiv  9558  uzin  9779  xaddval  10070  xnn0xadd0  10092  xnegdi  10093  xltadd1  10101  icc0r  10151  fznlem  10266  fseq1m1p1  10320  1fv  10364  fzon  10392  fvinim0ffz  10477  ioo0  10509  ico0  10511  ioc0  10512  flqbi  10540  divfl0  10546  modq0  10581  modqmuladdnn0  10620  addmodlteq  10650  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  seq3f1olemstep  10766  seq3f1olemp  10767  seq3id  10777  seq3z  10780  qsqeqor  10902  ccat0  11163  wrdl1s1  11197  ccatws1lenp1bg  11202  pfxsuff1eqwrdeq  11270  swrdccatin2  11300  pfxccatin12lem2  11302  mulreap  11415  rennim  11553  resqrexlemex  11576  rsqrmo  11578  resqrtcl  11580  rersqrtthlem  11581  sqrtsq2  11594  isumss  11942  fsum00  12013  telfsumo  12017  pwm1geoserap1  12059  prodssdc  12140  absefib  12322  efieq1re  12323  divides  12340  dvdsval2  12341  nndivides  12348  dvds0lem  12352  dvds1lem  12353  dvds2lem  12354  negdvdsb  12358  muldvds1  12367  muldvds2  12368  dvdscmulr  12371  dvdsmulcr  12372  dvdstr  12379  dvdsabseq  12398  divconjdvds  12400  odd2np1lem  12423  odd2np1  12424  even2n  12425  oddm1even  12426  2tp1odd  12435  opeo  12448  omeo  12449  m1exp1  12452  divalgb  12476  gcdaddm  12545  gcdabs1  12550  bezout  12572  gcdmultiple  12581  gcdmultiplez  12582  rplpwr  12588  rppwr  12589  nninfctlemfo  12601  alginv  12609  algcvga  12613  algfx  12614  eucalgval2  12615  coprmdvds  12654  qredeq  12658  qredeu  12659  divgcdcoprm0  12663  divgcdcoprmex  12664  cncongr1  12665  rpexp  12715  rpexp12i  12717  cncongrprm  12719  qnumdenbi  12754  phival  12775  phicl2  12776  dfphi2  12782  phiprmpw  12784  phimullem  12787  eulerthlem1  12789  eulerthlemfi  12790  eulerthlemrprm  12791  eulerthlemth  12794  eulerth  12795  fermltl  12796  hashgcdlem  12800  phisum  12803  odzval  12804  odzdvds  12808  reumodprminv  12816  modprm0  12817  nnnn0modprm0  12818  modprmn0modprm0  12819  coprimeprodsq  12820  coprimeprodsq2  12821  pythagtriplem2  12829  pythagtrip  12846  pceulem  12857  pcval  12859  pcqmul  12866  pcqcl  12869  pcabs  12889  pc2dvds  12893  pcaddlem  12902  pcadd  12903  pcmpt  12906  prmpwdvds  12918  pockthi  12921  4sqlem12  12965  ennnfonelemhf1o  13024  fvprif  13416  mgmidmo  13445  grpidvalg  13446  grpidpropdg  13447  ismgmid  13450  ismgmid2  13453  mgmidsssn0  13457  grpinvalem  13458  grprida  13460  igsumvalx  13462  gsumress  13468  ismnddef  13491  sgrpidmndm  13493  ismndd  13510  mndpropd  13513  mndinvmod  13518  mnd1  13528  ismhm  13534  gsumvallem2  13566  grpinvex  13583  isgrpd2  13594  isgrpd  13596  dfgrp2  13600  grpinveu  13611  grpinvval  13616  grplinv  13623  isgrpinv  13627  grplrinv  13630  grpidinv2  13631  grpidinv  13632  grplmulf1o  13647  grpsubeq0  13659  grpsubadd  13661  dfgrp3mlem  13671  dfgrp3m  13672  grp1  13679  imasgrp2  13687  qusgrp2  13690  mhmmnd  13693  ghmgrp  13695  mulgval  13699  mulgaddcom  13723  eqg0el  13806  ghmeqker  13848  ghmf1  13850  conjnmzb  13857  ablsubadd  13889  ablsubsub23  13902  rngmneg1  13950  rngmneg2  13951  dfur2g  13965  srgideu  13975  srgidmlem  13981  issrgid  13984  srgrz  13987  srglz  13988  srgisid  13989  srg1zr  13990  ringideu  14020  ringidmlem  14025  isringid  14028  ringid  14029  qusring2  14069  oppr0g  14084  oppr1g  14085  dvdsrvald  14097  dvdsrmuld  14100  dvdsr01  14108  dvdsr02  14109  opprunitd  14114  crngunit  14115  unitinvinv  14128  dvreq1  14146  dvdsrpropdg  14151  rhmdvdsr  14179  lringuplu  14200  subrg1  14235  subrgdvds  14239  isrrg  14267  rrgeq0i  14268  rrgeq0  14269  domneq0  14276  islmod  14295  islmodd  14297  lmodprop2d  14352  lss1d  14387  cnfldui  14593  znval  14640  znidom  14661  znunit  14663  znrrg  14664  mplelbascoe  14696  ntreq0  14846  ispsmet  15037  psmet0  15041  ismet  15058  isxmet  15059  xmeteq0  15073  metn0  15092  xmetres2  15093  xblss2ps  15118  xblss2  15119  xmseq0  15182  comet  15213  bdxmet  15215  cnmet  15244  ivthdec  15358  ivthreinc  15359  elply2  15449  reeff1o  15487  ioocosf1o  15568  logbgcd1irr  15681  logbgcd1irraplemexp  15682  mpodvdsmulf1o  15704  lgsval  15723  lgsdir  15754  lgsne0  15757  lgsprme0  15761  lgsdirnn0  15766  gausslemma2dlem0c  15770  gausslemma2dlem0i  15776  gausslemma2dlem7  15787  gausslemma2d  15788  lgseisenlem2  15790  lgseisenlem3  15791  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  lgsquad3  15803  m1lgs  15804  2lgs  15823  2sqlem7  15840  2sqlem8  15842  2sqlem9  15843  edg0iedg0g  15907  upgredg  15983  ushgredgedgloop  16067  edg0usgr  16086  vtxdgfval  16094  vtxdgop  16098  vtxdeqd  16102  vtxdfifiun  16103  vtxd0nedgbfi  16105  1loopgrvd2fi  16111  wksfval  16119  wlklenvclwlk  16170  clwwlknon  16224  isclwwlknon  16225  s2elclwwlknon2  16231  bj-charfunbi  16342  2omap  16530  pw1map  16532  pwle2  16535  subctctexmid  16537  peano4nninf  16544  nninfalllem1  16546  nninfsellemdc  16548  nninfsellemeq  16552  nninfsellemqall  16553  nninfsellemeqinf  16554  isomninnlem  16570  trilpolemlt1  16581  trirec0  16584  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  dceqnconst  16600  dcapnconst  16601