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  3839  preq12b  3847  preq12bg  3850  disji2  4074  invdisjrab  4076  iin0r  4252  opthg  4323  opeqsn  4338  unisucg  4504  opthreg  4647  tfisi  4678  dmsnopg  5199  relcoi1  5259  iotaeq  5286  iotabi  5287  fneq1  5408  fnun  5428  fnresdisj  5432  fnimadisj  5443  fnimaeq0  5444  sbcfng  5470  foeq1  5543  foco  5558  fveqeq2d  5634  fvelimab  5689  fvun1  5699  fvmptdv2  5723  fneqeql  5742  dffo3  5781  fvsng  5834  fconstfvm  5856  eufnfv  5869  f1veqaeq  5892  dff13f  5893  f1elima  5896  foeqcnvco  5913  f1eqcocnv  5914  acexmidlemab  5994  ovanraleqv  6024  eloprabga  6090  ovmpodv2  6137  ovi3  6141  ovelimab  6155  caovcang  6166  caovcan  6169  caovimo  6198  suppssfv  6212  suppssov1  6213  caofinvl  6242  caofid1  6245  caofid2  6246  uchoice  6281  op1stg  6294  op2ndg  6295  eqop  6321  reldm  6330  xporderlem  6375  tposfo2  6411  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  nnm0r  6623  nnmord  6661  nnaordex  6672  nnawordex  6673  ereq1  6685  eqerlem  6709  mapsn  6835  endisj  6979  pw2f1odclem  6991  xpf1o  7001  mapxpen  7005  fidifsnen  7028  supelti  7165  updjudhcoinlf  7243  updjudhcoinrg  7244  updjud  7245  omp1eomlem  7257  difinfsnlem  7262  nnnninfeq  7291  enomnilem  7301  finomni  7303  exmidomni  7305  fodjuomnilemres  7311  fodjuomni  7312  ismkvnex  7318  mkvprop  7321  fodjumkvlemres  7322  enmkvlem  7324  enwomnilem  7332  nninfdcinf  7334  nninfwlporlem  7336  nninfwlpoimlemginf  7339  pm54.43  7359  exmidfodomrlemrALT  7377  cc2lem  7448  addnidpig  7519  ltexpi  7520  dfplpq2  7537  dfmpq2  7538  recexnq  7573  recmulnqg  7574  ltexnqq  7591  halfnqq  7593  enq0tr  7617  nqnq0pi  7621  addnnnq0  7632  addlocpr  7719  ltexprlemru  7795  ltexpri  7796  lteupri  7800  prplnqu  7803  recexpr  7821  addsrpr  7928  mulsrpr  7929  00sr  7952  negexsr  7955  recexgt0sr  7956  srpospr  7966  prsrriota  7971  caucvgsrlemfv  7974  map2psrprg  7988  elrealeu  8012  axrnegex  8062  axprecex  8063  rereceu  8072  recriota  8073  nntopi  8077  axcaucvglemval  8080  axcaucvglemcau  8081  cnegexlem1  8317  cnegex  8320  cnegex2  8321  subval  8334  subadd  8345  subadd2  8346  subsub23  8347  addsubeq4  8357  subcan2  8367  negcon1  8394  subcan  8397  addrsub  8513  ltadd2  8562  ltordlem  8625  recexre  8721  recexap  8796  muleqadd  8811  receuap  8812  divvalap  8817  divmulap  8818  rec11ap  8853  rerecapb  8986  zdiv  9531  uzin  9751  xaddval  10037  xnn0xadd0  10059  xnegdi  10060  xltadd1  10068  icc0r  10118  fznlem  10233  fseq1m1p1  10287  1fv  10331  fzon  10359  fvinim0ffz  10442  ioo0  10474  ico0  10476  ioc0  10477  flqbi  10505  divfl0  10511  modq0  10546  modqmuladdnn0  10585  addmodlteq  10615  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  seq3f1olemstep  10731  seq3f1olemp  10732  seq3id  10742  seq3z  10745  qsqeqor  10867  ccat0  11126  wrdl1s1  11158  ccatws1lenp1bg  11163  pfxsuff1eqwrdeq  11226  swrdccatin2  11256  pfxccatin12lem2  11258  mulreap  11370  rennim  11508  resqrexlemex  11531  rsqrmo  11533  resqrtcl  11535  rersqrtthlem  11536  sqrtsq2  11549  isumss  11897  fsum00  11968  telfsumo  11972  pwm1geoserap1  12014  prodssdc  12095  absefib  12277  efieq1re  12278  divides  12295  dvdsval2  12296  nndivides  12303  dvds0lem  12307  dvds1lem  12308  dvds2lem  12309  negdvdsb  12313  muldvds1  12322  muldvds2  12323  dvdscmulr  12326  dvdsmulcr  12327  dvdstr  12334  dvdsabseq  12353  divconjdvds  12355  odd2np1lem  12378  odd2np1  12379  even2n  12380  oddm1even  12381  2tp1odd  12390  opeo  12403  omeo  12404  m1exp1  12407  divalgb  12431  gcdaddm  12500  gcdabs1  12505  bezout  12527  gcdmultiple  12536  gcdmultiplez  12537  rplpwr  12543  rppwr  12544  nninfctlemfo  12556  alginv  12564  algcvga  12568  algfx  12569  eucalgval2  12570  coprmdvds  12609  qredeq  12613  qredeu  12614  divgcdcoprm0  12618  divgcdcoprmex  12619  cncongr1  12620  rpexp  12670  rpexp12i  12672  cncongrprm  12674  qnumdenbi  12709  phival  12730  phicl2  12731  dfphi2  12737  phiprmpw  12739  phimullem  12742  eulerthlem1  12744  eulerthlemfi  12745  eulerthlemrprm  12746  eulerthlemth  12749  eulerth  12750  fermltl  12751  hashgcdlem  12755  phisum  12758  odzval  12759  odzdvds  12763  reumodprminv  12771  modprm0  12772  nnnn0modprm0  12773  modprmn0modprm0  12774  coprimeprodsq  12775  coprimeprodsq2  12776  pythagtriplem2  12784  pythagtrip  12801  pceulem  12812  pcval  12814  pcqmul  12821  pcqcl  12824  pcabs  12844  pc2dvds  12848  pcaddlem  12857  pcadd  12858  pcmpt  12861  prmpwdvds  12873  pockthi  12876  4sqlem12  12920  ennnfonelemhf1o  12979  fvprif  13371  mgmidmo  13400  grpidvalg  13401  grpidpropdg  13402  ismgmid  13405  ismgmid2  13408  mgmidsssn0  13412  grpinvalem  13413  grprida  13415  igsumvalx  13417  gsumress  13423  ismnddef  13446  sgrpidmndm  13448  ismndd  13465  mndpropd  13468  mndinvmod  13473  mnd1  13483  ismhm  13489  gsumvallem2  13521  grpinvex  13538  isgrpd2  13549  isgrpd  13551  dfgrp2  13555  grpinveu  13566  grpinvval  13571  grplinv  13578  isgrpinv  13582  grplrinv  13585  grpidinv2  13586  grpidinv  13587  grplmulf1o  13602  grpsubeq0  13614  grpsubadd  13616  dfgrp3mlem  13626  dfgrp3m  13627  grp1  13634  imasgrp2  13642  qusgrp2  13645  mhmmnd  13648  ghmgrp  13650  mulgval  13654  mulgaddcom  13678  eqg0el  13761  ghmeqker  13803  ghmf1  13805  conjnmzb  13812  ablsubadd  13844  ablsubsub23  13857  rngmneg1  13905  rngmneg2  13906  dfur2g  13920  srgideu  13930  srgidmlem  13936  issrgid  13939  srgrz  13942  srglz  13943  srgisid  13944  srg1zr  13945  ringideu  13975  ringidmlem  13980  isringid  13983  ringid  13984  qusring2  14024  oppr0g  14039  oppr1g  14040  reldvdsrsrg  14050  dvdsrvald  14051  dvdsrmuld  14054  dvdsr01  14062  dvdsr02  14063  opprunitd  14068  crngunit  14069  unitinvinv  14082  dvreq1  14100  dvdsrpropdg  14105  rhmdvdsr  14133  lringuplu  14154  subrg1  14189  subrgdvds  14193  isrrg  14221  rrgeq0i  14222  rrgeq0  14223  domneq0  14230  islmod  14249  islmodd  14251  lmodprop2d  14306  lss1d  14341  cnfldui  14547  znval  14594  znidom  14615  znunit  14617  znrrg  14618  mplelbascoe  14650  ntreq0  14800  ispsmet  14991  psmet0  14995  ismet  15012  isxmet  15013  xmeteq0  15027  metn0  15046  xmetres2  15047  xblss2ps  15072  xblss2  15073  xmseq0  15136  comet  15167  bdxmet  15169  cnmet  15198  ivthdec  15312  ivthreinc  15313  elply2  15403  reeff1o  15441  ioocosf1o  15522  logbgcd1irr  15635  logbgcd1irraplemexp  15636  mpodvdsmulf1o  15658  lgsval  15677  lgsdir  15708  lgsne0  15711  lgsprme0  15715  lgsdirnn0  15720  gausslemma2dlem0c  15724  gausslemma2dlem0i  15730  gausslemma2dlem7  15741  gausslemma2d  15742  lgseisenlem2  15744  lgseisenlem3  15745  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem2  15755  lgsquad3  15757  m1lgs  15758  2lgs  15777  2sqlem7  15794  2sqlem8  15796  2sqlem9  15797  edg0iedg0g  15860  upgredg  15936  ushgredgedgloop  16020  wksfval  16028  bj-charfunbi  16132  2omap  16318  pw1map  16320  pwle2  16323  subctctexmid  16325  peano4nninf  16331  nninfalllem1  16333  nninfsellemdc  16335  nninfsellemeq  16339  nninfsellemqall  16340  nninfsellemeqinf  16341  isomninnlem  16357  trilpolemlt1  16368  trirec0  16371  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379  dceqnconst  16387  dcapnconst  16388