Theorem eqeq1d 2213

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

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

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  rspcedeq1vd  2885  sbceq2g  3114  csbhypf  3131  csbiebt  3132  csbiebg  3135  dfss4st  3405  disjssun  3523  sneqrg  3802  preq12b  3810  preq12bg  3813  disji2  4036  iin0r  4212  opthg  4281  opeqsn  4295  unisucg  4459  opthreg  4602  tfisi  4633  dmsnopg  5151  relcoi1  5211  iotaeq  5237  iotabi  5238  fneq1  5356  fnun  5376  fnresdisj  5380  fnimadisj  5390  fnimaeq0  5391  sbcfng  5417  foeq1  5488  foco  5503  fveqeq2d  5578  fvelimab  5629  fvun1  5639  fvmptdv2  5663  fneqeql  5682  dffo3  5721  fvsng  5770  fconstfvm  5792  eufnfv  5805  f1veqaeq  5828  dff13f  5829  f1elima  5832  foeqcnvco  5849  f1eqcocnv  5850  acexmidlemab  5928  ovanraleqv  5958  eloprabga  6022  ovmpodv2  6069  ovi3  6073  ovelimab  6087  caovcang  6098  caovcan  6101  caovimo  6130  suppssfv  6144  suppssov1  6145  caofinvl  6174  caofid1  6177  caofid2  6178  uchoice  6213  op1stg  6226  op2ndg  6227  eqop  6253  reldm  6262  xporderlem  6307  tposfo2  6343  frec0g  6473  freccllem  6478  frecfcllem  6480  frecsuclem  6482  frecsuc  6483  nnm0r  6555  nnmord  6593  nnaordex  6604  nnawordex  6605  ereq1  6617  eqerlem  6641  mapsn  6767  endisj  6901  pw2f1odclem  6913  xpf1o  6923  mapxpen  6927  fidifsnen  6949  supelti  7086  updjudhcoinlf  7164  updjudhcoinrg  7165  updjud  7166  omp1eomlem  7178  difinfsnlem  7183  nnnninfeq  7212  enomnilem  7222  finomni  7224  exmidomni  7226  fodjuomnilemres  7232  fodjuomni  7233  ismkvnex  7239  mkvprop  7242  fodjumkvlemres  7243  enmkvlem  7245  enwomnilem  7253  nninfdcinf  7255  nninfwlporlem  7257  nninfwlpoimlemginf  7260  pm54.43  7280  exmidfodomrlemrALT  7293  cc2lem  7360  addnidpig  7431  ltexpi  7432  dfplpq2  7449  dfmpq2  7450  recexnq  7485  recmulnqg  7486  ltexnqq  7503  halfnqq  7505  enq0tr  7529  nqnq0pi  7533  addnnnq0  7544  addlocpr  7631  ltexprlemru  7707  ltexpri  7708  lteupri  7712  prplnqu  7715  recexpr  7733  addsrpr  7840  mulsrpr  7841  00sr  7864  negexsr  7867  recexgt0sr  7868  srpospr  7878  prsrriota  7883  caucvgsrlemfv  7886  map2psrprg  7900  elrealeu  7924  axrnegex  7974  axprecex  7975  rereceu  7984  recriota  7985  nntopi  7989  axcaucvglemval  7992  axcaucvglemcau  7993  cnegexlem1  8229  cnegex  8232  cnegex2  8233  subval  8246  subadd  8257  subadd2  8258  subsub23  8259  addsubeq4  8269  subcan2  8279  negcon1  8306  subcan  8309  addrsub  8425  ltadd2  8474  ltordlem  8537  recexre  8633  recexap  8708  muleqadd  8723  receuap  8724  divvalap  8729  divmulap  8730  rec11ap  8765  rerecapb  8898  zdiv  9443  uzin  9663  xaddval  9949  xnn0xadd0  9971  xnegdi  9972  xltadd1  9980  icc0r  10030  fznlem  10145  fseq1m1p1  10199  1fv  10243  fzon  10271  fvinim0ffz  10351  ioo0  10383  ico0  10385  ioc0  10386  flqbi  10414  divfl0  10420  modq0  10455  modqmuladdnn0  10494  addmodlteq  10524  frecuzrdgtcl  10538  frecuzrdgfunlem  10545  seq3f1olemstep  10640  seq3f1olemp  10641  seq3id  10651  seq3z  10654  qsqeqor  10776  ccat0  11027  mulreap  11094  rennim  11232  resqrexlemex  11255  rsqrmo  11257  resqrtcl  11259  rersqrtthlem  11260  sqrtsq2  11273  isumss  11621  fsum00  11692  telfsumo  11696  pwm1geoserap1  11738  prodssdc  11819  absefib  12001  efieq1re  12002  divides  12019  dvdsval2  12020  nndivides  12027  dvds0lem  12031  dvds1lem  12032  dvds2lem  12033  negdvdsb  12037  muldvds1  12046  muldvds2  12047  dvdscmulr  12050  dvdsmulcr  12051  dvdstr  12058  dvdsabseq  12077  divconjdvds  12079  odd2np1lem  12102  odd2np1  12103  even2n  12104  oddm1even  12105  2tp1odd  12114  opeo  12127  omeo  12128  m1exp1  12131  divalgb  12155  gcdaddm  12224  gcdabs1  12229  bezout  12251  gcdmultiple  12260  gcdmultiplez  12261  rplpwr  12267  rppwr  12268  nninfctlemfo  12280  alginv  12288  algcvga  12292  algfx  12293  eucalgval2  12294  coprmdvds  12333  qredeq  12337  qredeu  12338  divgcdcoprm0  12342  divgcdcoprmex  12343  cncongr1  12344  rpexp  12394  rpexp12i  12396  cncongrprm  12398  qnumdenbi  12433  phival  12454  phicl2  12455  dfphi2  12461  phiprmpw  12463  phimullem  12466  eulerthlem1  12468  eulerthlemfi  12469  eulerthlemrprm  12470  eulerthlemth  12473  eulerth  12474  fermltl  12475  hashgcdlem  12479  phisum  12482  odzval  12483  odzdvds  12487  reumodprminv  12495  modprm0  12496  nnnn0modprm0  12497  modprmn0modprm0  12498  coprimeprodsq  12499  coprimeprodsq2  12500  pythagtriplem2  12508  pythagtrip  12525  pceulem  12536  pcval  12538  pcqmul  12545  pcqcl  12548  pcabs  12568  pc2dvds  12572  pcaddlem  12581  pcadd  12582  pcmpt  12585  prmpwdvds  12597  pockthi  12600  4sqlem12  12644  ennnfonelemhf1o  12703  fvprif  13093  mgmidmo  13122  grpidvalg  13123  grpidpropdg  13124  ismgmid  13127  ismgmid2  13130  mgmidsssn0  13134  grpinvalem  13135  grprida  13137  igsumvalx  13139  gsumress  13145  ismnddef  13168  sgrpidmndm  13170  ismndd  13187  mndpropd  13190  mndinvmod  13195  mnd1  13205  ismhm  13211  gsumvallem2  13243  grpinvex  13260  isgrpd2  13271  isgrpd  13273  dfgrp2  13277  grpinveu  13288  grpinvval  13293  grplinv  13300  isgrpinv  13304  grplrinv  13307  grpidinv2  13308  grpidinv  13309  grplmulf1o  13324  grpsubeq0  13336  grpsubadd  13338  dfgrp3mlem  13348  dfgrp3m  13349  grp1  13356  imasgrp2  13364  qusgrp2  13367  mhmmnd  13370  ghmgrp  13372  mulgval  13376  mulgaddcom  13400  eqg0el  13483  ghmeqker  13525  ghmf1  13527  conjnmzb  13534  ablsubadd  13566  ablsubsub23  13579  rngmneg1  13627  rngmneg2  13628  dfur2g  13642  srgideu  13652  srgidmlem  13658  issrgid  13661  srgrz  13664  srglz  13665  srgisid  13666  srg1zr  13667  ringideu  13697  ringidmlem  13702  isringid  13705  ringid  13706  qusring2  13746  oppr0g  13761  oppr1g  13762  reldvdsrsrg  13772  dvdsrvald  13773  dvdsrmuld  13776  dvdsr01  13784  dvdsr02  13785  opprunitd  13790  crngunit  13791  unitinvinv  13804  dvreq1  13822  dvdsrpropdg  13827  rhmdvdsr  13855  lringuplu  13876  subrg1  13911  subrgdvds  13915  isrrg  13943  rrgeq0i  13944  rrgeq0  13945  domneq0  13952  islmod  13971  islmodd  13973  lmodprop2d  14028  lss1d  14063  cnfldui  14269  znval  14316  znidom  14337  znunit  14339  znrrg  14340  mplelbascoe  14372  ntreq0  14522  ispsmet  14713  psmet0  14717  ismet  14734  isxmet  14735  xmeteq0  14749  metn0  14768  xmetres2  14769  xblss2ps  14794  xblss2  14795  xmseq0  14858  comet  14889  bdxmet  14891  cnmet  14920  ivthdec  15034  ivthreinc  15035  elply2  15125  reeff1o  15163  ioocosf1o  15244  logbgcd1irr  15357  logbgcd1irraplemexp  15358  mpodvdsmulf1o  15380  lgsval  15399  lgsdir  15430  lgsne0  15433  lgsprme0  15437  lgsdirnn0  15442  gausslemma2dlem0c  15446  gausslemma2dlem0i  15452  gausslemma2dlem7  15463  gausslemma2d  15464  lgseisenlem2  15466  lgseisenlem3  15467  lgsquadlem1  15472  lgsquadlem2  15473  lgsquad2lem2  15477  lgsquad3  15479  m1lgs  15480  2lgs  15499  2sqlem7  15516  2sqlem8  15518  2sqlem9  15519  bj-charfunbi  15611  2omap  15796  pwle2  15799  subctctexmid  15801  peano4nninf  15807  nninfalllem1  15809  nninfsellemdc  15811  nninfsellemeq  15815  nninfsellemqall  15816  nninfsellemeqinf  15817  isomninnlem  15833  trilpolemlt1  15844  trirec0  15847  iswomninnlem  15852  iswomni0  15854  ismkvnnlem  15855  dceqnconst  15863  dcapnconst  15864