Theorem eqeq1d 2205

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  rspcedeq1vd  2877  sbceq2g  3106  csbhypf  3123  csbiebt  3124  csbiebg  3127  dfss4st  3397  disjssun  3515  sneqrg  3793  preq12b  3801  preq12bg  3804  disji2  4027  iin0r  4203  opthg  4272  opeqsn  4286  unisucg  4450  opthreg  4593  tfisi  4624  dmsnopg  5142  relcoi1  5202  iotaeq  5228  iotabi  5229  fneq1  5347  fnun  5367  fnresdisj  5371  fnimadisj  5381  fnimaeq0  5382  sbcfng  5408  foeq1  5479  foco  5494  fveqeq2d  5569  fvelimab  5620  fvun1  5630  fvmptdv2  5654  fneqeql  5673  dffo3  5712  fvsng  5761  fconstfvm  5783  eufnfv  5796  f1veqaeq  5819  dff13f  5820  f1elima  5823  foeqcnvco  5840  f1eqcocnv  5841  acexmidlemab  5919  ovanraleqv  5949  eloprabga  6013  ovmpodv2  6060  ovi3  6064  ovelimab  6078  caovcang  6089  caovcan  6092  caovimo  6121  suppssfv  6135  suppssov1  6136  caofinvl  6165  caofid1  6168  caofid2  6169  uchoice  6204  op1stg  6217  op2ndg  6218  eqop  6244  reldm  6253  xporderlem  6298  tposfo2  6334  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnm0r  6546  nnmord  6584  nnaordex  6595  nnawordex  6596  ereq1  6608  eqerlem  6632  mapsn  6758  endisj  6892  pw2f1odclem  6904  xpf1o  6914  mapxpen  6918  fidifsnen  6940  supelti  7077  updjudhcoinlf  7155  updjudhcoinrg  7156  updjud  7157  omp1eomlem  7169  difinfsnlem  7174  nnnninfeq  7203  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  fodjuomni  7224  ismkvnex  7230  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemginf  7251  pm54.43  7271  exmidfodomrlemrALT  7284  cc2lem  7351  addnidpig  7422  ltexpi  7423  dfplpq2  7440  dfmpq2  7441  recexnq  7476  recmulnqg  7477  ltexnqq  7494  halfnqq  7496  enq0tr  7520  nqnq0pi  7524  addnnnq0  7535  addlocpr  7622  ltexprlemru  7698  ltexpri  7699  lteupri  7703  prplnqu  7706  recexpr  7724  addsrpr  7831  mulsrpr  7832  00sr  7855  negexsr  7858  recexgt0sr  7859  srpospr  7869  prsrriota  7874  caucvgsrlemfv  7877  map2psrprg  7891  elrealeu  7915  axrnegex  7965  axprecex  7966  rereceu  7975  recriota  7976  nntopi  7980  axcaucvglemval  7983  axcaucvglemcau  7984  cnegexlem1  8220  cnegex  8223  cnegex2  8224  subval  8237  subadd  8248  subadd2  8249  subsub23  8250  addsubeq4  8260  subcan2  8270  negcon1  8297  subcan  8300  addrsub  8416  ltadd2  8465  ltordlem  8528  recexre  8624  recexap  8699  muleqadd  8714  receuap  8715  divvalap  8720  divmulap  8721  rec11ap  8756  rerecapb  8889  zdiv  9433  uzin  9653  xaddval  9939  xnn0xadd0  9961  xnegdi  9962  xltadd1  9970  icc0r  10020  fznlem  10135  fseq1m1p1  10189  1fv  10233  fzon  10261  fvinim0ffz  10336  ioo0  10368  ico0  10370  ioc0  10371  flqbi  10399  divfl0  10405  modq0  10440  modqmuladdnn0  10479  addmodlteq  10509  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  seq3f1olemstep  10625  seq3f1olemp  10626  seq3id  10636  seq3z  10639  qsqeqor  10761  mulreap  11048  rennim  11186  resqrexlemex  11209  rsqrmo  11211  resqrtcl  11213  rersqrtthlem  11214  sqrtsq2  11227  isumss  11575  fsum00  11646  telfsumo  11650  pwm1geoserap1  11692  prodssdc  11773  absefib  11955  efieq1re  11956  divides  11973  dvdsval2  11974  nndivides  11981  dvds0lem  11985  dvds1lem  11986  dvds2lem  11987  negdvdsb  11991  muldvds1  12000  muldvds2  12001  dvdscmulr  12004  dvdsmulcr  12005  dvdstr  12012  dvdsabseq  12031  divconjdvds  12033  odd2np1lem  12056  odd2np1  12057  even2n  12058  oddm1even  12059  2tp1odd  12068  opeo  12081  omeo  12082  m1exp1  12085  divalgb  12109  gcdaddm  12178  gcdabs1  12183  bezout  12205  gcdmultiple  12214  gcdmultiplez  12215  rplpwr  12221  rppwr  12222  nninfctlemfo  12234  alginv  12242  algcvga  12246  algfx  12247  eucalgval2  12248  coprmdvds  12287  qredeq  12291  qredeu  12292  divgcdcoprm0  12296  divgcdcoprmex  12297  cncongr1  12298  rpexp  12348  rpexp12i  12350  cncongrprm  12352  qnumdenbi  12387  phival  12408  phicl2  12409  dfphi2  12415  phiprmpw  12417  phimullem  12420  eulerthlem1  12422  eulerthlemfi  12423  eulerthlemrprm  12424  eulerthlemth  12427  eulerth  12428  fermltl  12429  hashgcdlem  12433  phisum  12436  odzval  12437  odzdvds  12441  reumodprminv  12449  modprm0  12450  nnnn0modprm0  12451  modprmn0modprm0  12452  coprimeprodsq  12453  coprimeprodsq2  12454  pythagtriplem2  12462  pythagtrip  12479  pceulem  12490  pcval  12492  pcqmul  12499  pcqcl  12502  pcabs  12522  pc2dvds  12526  pcaddlem  12535  pcadd  12536  pcmpt  12539  prmpwdvds  12551  pockthi  12554  4sqlem12  12598  ennnfonelemhf1o  12657  fvprif  13047  mgmidmo  13076  grpidvalg  13077  grpidpropdg  13078  ismgmid  13081  ismgmid2  13084  mgmidsssn0  13088  grpinvalem  13089  grprida  13091  igsumvalx  13093  gsumress  13099  ismnddef  13122  sgrpidmndm  13124  ismndd  13141  mndpropd  13144  mndinvmod  13149  mnd1  13159  ismhm  13165  gsumvallem2  13197  grpinvex  13214  isgrpd2  13225  isgrpd  13227  dfgrp2  13231  grpinveu  13242  grpinvval  13247  grplinv  13254  isgrpinv  13258  grplrinv  13261  grpidinv2  13262  grpidinv  13263  grplmulf1o  13278  grpsubeq0  13290  grpsubadd  13292  dfgrp3mlem  13302  dfgrp3m  13303  grp1  13310  imasgrp2  13318  qusgrp2  13321  mhmmnd  13324  ghmgrp  13326  mulgval  13330  mulgaddcom  13354  eqg0el  13437  ghmeqker  13479  ghmf1  13481  conjnmzb  13488  ablsubadd  13520  ablsubsub23  13533  rngmneg1  13581  rngmneg2  13582  dfur2g  13596  srgideu  13606  srgidmlem  13612  issrgid  13615  srgrz  13618  srglz  13619  srgisid  13620  srg1zr  13621  ringideu  13651  ringidmlem  13656  isringid  13659  ringid  13660  qusring2  13700  oppr0g  13715  oppr1g  13716  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrmuld  13730  dvdsr01  13738  dvdsr02  13739  opprunitd  13744  crngunit  13745  unitinvinv  13758  dvreq1  13776  dvdsrpropdg  13781  rhmdvdsr  13809  lringuplu  13830  subrg1  13865  subrgdvds  13869  isrrg  13897  rrgeq0i  13898  rrgeq0  13899  domneq0  13906  islmod  13925  islmodd  13927  lmodprop2d  13982  lss1d  14017  cnfldui  14223  znval  14270  znidom  14291  znunit  14293  znrrg  14294  mplelbascoe  14326  ntreq0  14476  ispsmet  14667  psmet0  14671  ismet  14688  isxmet  14689  xmeteq0  14703  metn0  14722  xmetres2  14723  xblss2ps  14748  xblss2  14749  xmseq0  14812  comet  14843  bdxmet  14845  cnmet  14874  ivthdec  14988  ivthreinc  14989  elply2  15079  reeff1o  15117  ioocosf1o  15198  logbgcd1irr  15311  logbgcd1irraplemexp  15312  mpodvdsmulf1o  15334  lgsval  15353  lgsdir  15384  lgsne0  15387  lgsprme0  15391  lgsdirnn0  15396  gausslemma2dlem0c  15400  gausslemma2dlem0i  15406  gausslemma2dlem7  15417  gausslemma2d  15418  lgseisenlem2  15420  lgseisenlem3  15421  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem2  15431  lgsquad3  15433  m1lgs  15434  2lgs  15453  2sqlem7  15470  2sqlem8  15472  2sqlem9  15473  bj-charfunbi  15565  2omap  15750  pwle2  15753  subctctexmid  15755  peano4nninf  15761  nninfalllem1  15763  nninfsellemdc  15765  nninfsellemeq  15769  nninfsellemqall  15770  nninfsellemeqinf  15771  isomninnlem  15787  trilpolemlt1  15798  trirec0  15801  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809  dceqnconst  15817  dcapnconst  15818