Theorem eqeq1d 2241

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  rspcedeq1vd  2930  sbceq2g  3160  csbhypf  3177  csbiebt  3178  csbiebg  3181  dfss4st  3454  disjssun  3572  sneqrg  3866  preq12b  3874  preq12bg  3877  disji2  4101  invdisjrab  4103  iin0r  4282  opthg  4354  opeqsn  4369  unisucg  4535  opthreg  4678  tfisi  4709  dmsnopg  5234  relcoi1  5294  iotaeq  5321  iotabi  5322  fneq1  5444  fnun  5464  fnresdisj  5468  fnimadisj  5479  fnimaeq0  5480  sbcfng  5506  foeq1  5586  foco  5601  fveqeq2d  5678  fvelimab  5733  fvun1  5743  fvmptdv2  5767  fneqeql  5786  dffo3  5824  fvsng  5880  fconstfvm  5902  eufnfv  5917  f1veqaeq  5942  dff13f  5943  f1elima  5946  foeqcnvco  5963  f1eqcocnv  5964  acexmidlemab  6044  ovanraleqv  6074  eloprabga  6140  ovmpodv2  6187  ovi3  6191  ovelimab  6205  caovcang  6216  caovcan  6219  caovimo  6248  suppssov1  6263  caofinvl  6292  caofid1  6295  caofid2  6296  uchoice  6331  op1stg  6344  op2ndg  6345  eqop  6371  reldm  6380  xporderlem  6427  suppofss1dcl  6464  suppofss2dcl  6465  tposfo2  6498  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  nnm0r  6712  nnmord  6750  nnaordex  6761  nnawordex  6762  ereq1  6774  eqerlem  6798  mapsnd  6923  mapsn  6925  endisj  7075  pw2f1odclem  7087  xpf1o  7097  mapxpen  7101  fidifsnen  7125  2omap  7269  supelti  7293  updjudhcoinlf  7371  updjudhcoinrg  7372  updjud  7373  omp1eomlem  7385  difinfsnlem  7390  nnnninfeq  7419  enomnilem  7429  finomni  7431  exmidomni  7433  fodjuomnilemres  7439  fodjuomni  7440  ismkvnex  7446  mkvprop  7449  fodjumkvlemres  7450  enmkvlem  7452  enwomnilem  7460  nninfdcinf  7462  nninfwlporlem  7464  nninfwlpoimlemginf  7467  pm54.43  7487  exmidfodomrlemrALT  7506  cc2lem  7580  addnidpig  7651  ltexpi  7652  dfplpq2  7669  dfmpq2  7670  recexnq  7705  recmulnqg  7706  ltexnqq  7723  halfnqq  7725  enq0tr  7749  nqnq0pi  7753  addnnnq0  7764  addlocpr  7851  ltexprlemru  7927  ltexpri  7928  lteupri  7932  prplnqu  7935  recexpr  7953  addsrpr  8060  mulsrpr  8061  00sr  8084  negexsr  8087  recexgt0sr  8088  srpospr  8098  prsrriota  8103  caucvgsrlemfv  8106  map2psrprg  8120  elrealeu  8144  axrnegex  8194  axprecex  8195  rereceu  8204  recriota  8205  nntopi  8209  axcaucvglemval  8212  axcaucvglemcau  8213  cnegexlem1  8448  cnegex  8451  cnegex2  8452  subval  8465  subadd  8476  subadd2  8477  subsub23  8478  addsubeq4  8488  subcan2  8498  negcon1  8525  subcan  8528  addrsub  8644  ltadd2  8693  ltordlem  8756  recexre  8852  recexap  8927  muleqadd  8942  receuap  8943  divvalap  8948  divmulap  8949  rec11ap  8984  rerecapb  9117  zdiv  9666  uzin  9887  xaddval  10178  xnn0xadd0  10200  xnegdi  10201  xltadd1  10209  icc0r  10259  fznlem  10375  fseq1m1p1  10429  1fv  10473  fzon  10501  fvinim0ffz  10587  ioo0  10619  ico0  10621  ioc0  10622  flqbi  10650  divfl0  10656  modq0  10691  modqmuladdnn0  10730  addmodlteq  10760  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  seq3f1olemstep  10876  seq3f1olemp  10877  seq3id  10887  seq3z  10890  qsqeqor  11012  hashfibc  11207  hashtpglem  11218  ccat0  11284  wrdl1s1  11318  ccatws1lenp1bg  11323  pfxsuff1eqwrdeq  11391  swrdccatin2  11421  pfxccatin12lem2  11423  mulreap  11549  rennim  11687  resqrexlemex  11710  rsqrmo  11712  resqrtcl  11714  rersqrtthlem  11715  sqrtsq2  11728  isumss  12077  fsum00  12148  telfsumo  12152  pwm1geoserap1  12194  prodssdc  12275  absefib  12457  efieq1re  12458  divides  12475  dvdsval2  12476  nndivides  12483  dvds0lem  12487  dvds1lem  12488  dvds2lem  12489  negdvdsb  12493  muldvds1  12502  muldvds2  12503  dvdscmulr  12506  dvdsmulcr  12507  dvdstr  12514  dvdsabseq  12533  divconjdvds  12535  odd2np1lem  12558  odd2np1  12559  even2n  12560  oddm1even  12561  2tp1odd  12570  opeo  12583  omeo  12584  m1exp1  12587  divalgb  12611  gcdaddm  12680  gcdabs1  12685  bezout  12707  gcdmultiple  12716  gcdmultiplez  12717  rplpwr  12723  rppwr  12724  nninfctlemfo  12736  alginv  12744  algcvga  12748  algfx  12749  eucalgval2  12750  coprmdvds  12789  qredeq  12793  qredeu  12794  divgcdcoprm0  12798  divgcdcoprmex  12799  cncongr1  12800  rpexp  12850  rpexp12i  12852  cncongrprm  12854  qnumdenbi  12889  phival  12910  phicl2  12911  dfphi2  12917  phiprmpw  12919  phimullem  12922  eulerthlem1  12924  eulerthlemfi  12925  eulerthlemrprm  12926  eulerthlemth  12929  eulerth  12930  fermltl  12931  hashgcdlem  12935  phisum  12938  odzval  12939  odzdvds  12943  reumodprminv  12951  modprm0  12952  nnnn0modprm0  12953  modprmn0modprm0  12954  coprimeprodsq  12955  coprimeprodsq2  12956  pythagtriplem2  12964  pythagtrip  12981  pceulem  12992  pcval  12994  pcqmul  13001  pcqcl  13004  pcabs  13024  pc2dvds  13028  pcaddlem  13037  pcadd  13038  pcmpt  13041  prmpwdvds  13053  pockthi  13056  4sqlem12  13100  ennnfonelemhf1o  13164  fvprif  13556  mgmidmo  13585  grpidvalg  13586  grpidpropdg  13587  ismgmid  13590  ismgmid2  13593  mgmidsssn0  13597  grpinvalem  13598  grprida  13600  igsumvalx  13602  gsumress  13608  ismnddef  13631  sgrpidmndm  13633  ismndd  13650  mndpropd  13653  mndinvmod  13658  mnd1  13668  ismhm  13674  gsumvallem2  13706  grpinvex  13723  isgrpd2  13734  isgrpd  13736  dfgrp2  13740  grpinveu  13751  grpinvval  13756  grplinv  13763  isgrpinv  13767  grplrinv  13770  grpidinv2  13771  grpidinv  13772  grplmulf1o  13787  grpsubeq0  13799  grpsubadd  13801  dfgrp3mlem  13811  dfgrp3m  13812  grp1  13819  imasgrp2  13827  qusgrp2  13830  mhmmnd  13833  ghmgrp  13835  mulgval  13839  mulgaddcom  13863  eqg0el  13946  ghmeqker  13988  ghmf1  13990  conjnmzb  13997  ablsubadd  14029  ablsubsub23  14042  rngmneg1  14091  rngmneg2  14092  dfur2g  14106  srgideu  14116  srgidmlem  14122  issrgid  14125  srgrz  14128  srglz  14129  srgisid  14130  srg1zr  14131  ringideu  14161  ringidmlem  14166  isringid  14169  ringid  14170  qusring2  14210  oppr0g  14225  oppr1g  14226  dvdsrvald  14238  dvdsrmuld  14241  dvdsr01  14249  dvdsr02  14250  opprunitd  14255  crngunit  14256  unitinvinv  14269  dvreq1  14287  dvdsrpropdg  14292  rhmdvdsr  14320  lringuplu  14341  subrg1  14376  subrgdvds  14380  isrrg  14408  rrgeq0i  14409  rrgeq0  14410  domneq0  14418  islmod  14439  islmodd  14441  lmodprop2d  14496  lss1d  14531  cnfldui  14737  znval  14784  znidom  14805  znunit  14807  znrrg  14808  mplelbascoe  14847  ntreq0  14997  ispsmet  15188  psmet0  15192  ismet  15209  isxmet  15210  xmeteq0  15224  metn0  15243  xmetres2  15244  xblss2ps  15269  xblss2  15270  xmseq0  15333  comet  15364  bdxmet  15366  cnmet  15395  ivthdec  15509  ivthreinc  15510  elply2  15600  reeff1o  15638  ioocosf1o  15719  logbgcd1irr  15832  logbgcd1irraplemexp  15833  mpodvdsmulf1o  15858  lgsval  15877  lgsdir  15908  lgsne0  15911  lgsprme0  15915  lgsdirnn0  15920  gausslemma2dlem0c  15924  gausslemma2dlem0i  15930  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem2  15944  lgseisenlem3  15945  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  lgsquad3  15957  m1lgs  15958  2lgs  15977  2sqlem7  15994  2sqlem8  15996  2sqlem9  15997  edg0iedg0g  16061  upgredg  16139  ushgredgedgloop  16223  edg0usgr  16242  vtxdgfval  16283  vtxdgop  16287  vtxdeqd  16291  vtxdfifiun  16292  vtxd0nedgbfi  16294  1loopgrvd2fi  16300  wksfval  16317  wlklenvclwlk  16368  clwwlknon  16424  isclwwlknon  16425  s2elclwwlknon2  16431  depind  16504  bj-charfunbi  16581  pw1map  16769  pwle2  16772  subctctexmid  16774  peano4nninf  16784  nninfalllem1  16786  nninfsellemdc  16788  nninfsellemeq  16792  nninfsellemqall  16793  nninfsellemeqinf  16794  isomninnlem  16814  trilpolemlt1  16825  trirec0  16828  qdiff  16833  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837  dceqnconst  16846  dcapnconst  16847  gfsumz  16869