Theorem eqeq1d 2215

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  rspcedeq1vd  2890  sbceq2g  3119  csbhypf  3136  csbiebt  3137  csbiebg  3140  dfss4st  3410  disjssun  3528  sneqrg  3809  preq12b  3817  preq12bg  3820  disji2  4043  invdisjrab  4045  iin0r  4221  opthg  4290  opeqsn  4305  unisucg  4469  opthreg  4612  tfisi  4643  dmsnopg  5163  relcoi1  5223  iotaeq  5249  iotabi  5250  fneq1  5371  fnun  5391  fnresdisj  5395  fnimadisj  5406  fnimaeq0  5407  sbcfng  5433  foeq1  5506  foco  5521  fveqeq2d  5597  fvelimab  5648  fvun1  5658  fvmptdv2  5682  fneqeql  5701  dffo3  5740  fvsng  5793  fconstfvm  5815  eufnfv  5828  f1veqaeq  5851  dff13f  5852  f1elima  5855  foeqcnvco  5872  f1eqcocnv  5873  acexmidlemab  5951  ovanraleqv  5981  eloprabga  6045  ovmpodv2  6092  ovi3  6096  ovelimab  6110  caovcang  6121  caovcan  6124  caovimo  6153  suppssfv  6167  suppssov1  6168  caofinvl  6197  caofid1  6200  caofid2  6201  uchoice  6236  op1stg  6249  op2ndg  6250  eqop  6276  reldm  6285  xporderlem  6330  tposfo2  6366  frec0g  6496  freccllem  6501  frecfcllem  6503  frecsuclem  6505  frecsuc  6506  nnm0r  6578  nnmord  6616  nnaordex  6627  nnawordex  6628  ereq1  6640  eqerlem  6664  mapsn  6790  endisj  6934  pw2f1odclem  6946  xpf1o  6956  mapxpen  6960  fidifsnen  6982  supelti  7119  updjudhcoinlf  7197  updjudhcoinrg  7198  updjud  7199  omp1eomlem  7211  difinfsnlem  7216  nnnninfeq  7245  enomnilem  7255  finomni  7257  exmidomni  7259  fodjuomnilemres  7265  fodjuomni  7266  ismkvnex  7272  mkvprop  7275  fodjumkvlemres  7276  enmkvlem  7278  enwomnilem  7286  nninfdcinf  7288  nninfwlporlem  7290  nninfwlpoimlemginf  7293  pm54.43  7313  exmidfodomrlemrALT  7327  cc2lem  7398  addnidpig  7469  ltexpi  7470  dfplpq2  7487  dfmpq2  7488  recexnq  7523  recmulnqg  7524  ltexnqq  7541  halfnqq  7543  enq0tr  7567  nqnq0pi  7571  addnnnq0  7582  addlocpr  7669  ltexprlemru  7745  ltexpri  7746  lteupri  7750  prplnqu  7753  recexpr  7771  addsrpr  7878  mulsrpr  7879  00sr  7902  negexsr  7905  recexgt0sr  7906  srpospr  7916  prsrriota  7921  caucvgsrlemfv  7924  map2psrprg  7938  elrealeu  7962  axrnegex  8012  axprecex  8013  rereceu  8022  recriota  8023  nntopi  8027  axcaucvglemval  8030  axcaucvglemcau  8031  cnegexlem1  8267  cnegex  8270  cnegex2  8271  subval  8284  subadd  8295  subadd2  8296  subsub23  8297  addsubeq4  8307  subcan2  8317  negcon1  8344  subcan  8347  addrsub  8463  ltadd2  8512  ltordlem  8575  recexre  8671  recexap  8746  muleqadd  8761  receuap  8762  divvalap  8767  divmulap  8768  rec11ap  8803  rerecapb  8936  zdiv  9481  uzin  9701  xaddval  9987  xnn0xadd0  10009  xnegdi  10010  xltadd1  10018  icc0r  10068  fznlem  10183  fseq1m1p1  10237  1fv  10281  fzon  10309  fvinim0ffz  10392  ioo0  10424  ico0  10426  ioc0  10427  flqbi  10455  divfl0  10461  modq0  10496  modqmuladdnn0  10535  addmodlteq  10565  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  seq3f1olemstep  10681  seq3f1olemp  10682  seq3id  10692  seq3z  10695  qsqeqor  10817  ccat0  11075  wrdl1s1  11107  ccatws1lenp1bg  11112  pfxsuff1eqwrdeq  11175  mulreap  11250  rennim  11388  resqrexlemex  11411  rsqrmo  11413  resqrtcl  11415  rersqrtthlem  11416  sqrtsq2  11429  isumss  11777  fsum00  11848  telfsumo  11852  pwm1geoserap1  11894  prodssdc  11975  absefib  12157  efieq1re  12158  divides  12175  dvdsval2  12176  nndivides  12183  dvds0lem  12187  dvds1lem  12188  dvds2lem  12189  negdvdsb  12193  muldvds1  12202  muldvds2  12203  dvdscmulr  12206  dvdsmulcr  12207  dvdstr  12214  dvdsabseq  12233  divconjdvds  12235  odd2np1lem  12258  odd2np1  12259  even2n  12260  oddm1even  12261  2tp1odd  12270  opeo  12283  omeo  12284  m1exp1  12287  divalgb  12311  gcdaddm  12380  gcdabs1  12385  bezout  12407  gcdmultiple  12416  gcdmultiplez  12417  rplpwr  12423  rppwr  12424  nninfctlemfo  12436  alginv  12444  algcvga  12448  algfx  12449  eucalgval2  12450  coprmdvds  12489  qredeq  12493  qredeu  12494  divgcdcoprm0  12498  divgcdcoprmex  12499  cncongr1  12500  rpexp  12550  rpexp12i  12552  cncongrprm  12554  qnumdenbi  12589  phival  12610  phicl2  12611  dfphi2  12617  phiprmpw  12619  phimullem  12622  eulerthlem1  12624  eulerthlemfi  12625  eulerthlemrprm  12626  eulerthlemth  12629  eulerth  12630  fermltl  12631  hashgcdlem  12635  phisum  12638  odzval  12639  odzdvds  12643  reumodprminv  12651  modprm0  12652  nnnn0modprm0  12653  modprmn0modprm0  12654  coprimeprodsq  12655  coprimeprodsq2  12656  pythagtriplem2  12664  pythagtrip  12681  pceulem  12692  pcval  12694  pcqmul  12701  pcqcl  12704  pcabs  12724  pc2dvds  12728  pcaddlem  12737  pcadd  12738  pcmpt  12741  prmpwdvds  12753  pockthi  12756  4sqlem12  12800  ennnfonelemhf1o  12859  fvprif  13250  mgmidmo  13279  grpidvalg  13280  grpidpropdg  13281  ismgmid  13284  ismgmid2  13287  mgmidsssn0  13291  grpinvalem  13292  grprida  13294  igsumvalx  13296  gsumress  13302  ismnddef  13325  sgrpidmndm  13327  ismndd  13344  mndpropd  13347  mndinvmod  13352  mnd1  13362  ismhm  13368  gsumvallem2  13400  grpinvex  13417  isgrpd2  13428  isgrpd  13430  dfgrp2  13434  grpinveu  13445  grpinvval  13450  grplinv  13457  isgrpinv  13461  grplrinv  13464  grpidinv2  13465  grpidinv  13466  grplmulf1o  13481  grpsubeq0  13493  grpsubadd  13495  dfgrp3mlem  13505  dfgrp3m  13506  grp1  13513  imasgrp2  13521  qusgrp2  13524  mhmmnd  13527  ghmgrp  13529  mulgval  13533  mulgaddcom  13557  eqg0el  13640  ghmeqker  13682  ghmf1  13684  conjnmzb  13691  ablsubadd  13723  ablsubsub23  13736  rngmneg1  13784  rngmneg2  13785  dfur2g  13799  srgideu  13809  srgidmlem  13815  issrgid  13818  srgrz  13821  srglz  13822  srgisid  13823  srg1zr  13824  ringideu  13854  ringidmlem  13859  isringid  13862  ringid  13863  qusring2  13903  oppr0g  13918  oppr1g  13919  reldvdsrsrg  13929  dvdsrvald  13930  dvdsrmuld  13933  dvdsr01  13941  dvdsr02  13942  opprunitd  13947  crngunit  13948  unitinvinv  13961  dvreq1  13979  dvdsrpropdg  13984  rhmdvdsr  14012  lringuplu  14033  subrg1  14068  subrgdvds  14072  isrrg  14100  rrgeq0i  14101  rrgeq0  14102  domneq0  14109  islmod  14128  islmodd  14130  lmodprop2d  14185  lss1d  14220  cnfldui  14426  znval  14473  znidom  14494  znunit  14496  znrrg  14497  mplelbascoe  14529  ntreq0  14679  ispsmet  14870  psmet0  14874  ismet  14891  isxmet  14892  xmeteq0  14906  metn0  14925  xmetres2  14926  xblss2ps  14951  xblss2  14952  xmseq0  15015  comet  15046  bdxmet  15048  cnmet  15077  ivthdec  15191  ivthreinc  15192  elply2  15282  reeff1o  15320  ioocosf1o  15401  logbgcd1irr  15514  logbgcd1irraplemexp  15515  mpodvdsmulf1o  15537  lgsval  15556  lgsdir  15587  lgsne0  15590  lgsprme0  15594  lgsdirnn0  15599  gausslemma2dlem0c  15603  gausslemma2dlem0i  15609  gausslemma2dlem7  15620  gausslemma2d  15621  lgseisenlem2  15623  lgseisenlem3  15624  lgsquadlem1  15629  lgsquadlem2  15630  lgsquad2lem2  15634  lgsquad3  15636  m1lgs  15637  2lgs  15656  2sqlem7  15673  2sqlem8  15675  2sqlem9  15676  edg0iedg0g  15737  bj-charfunbi  15885  2omap  16071  pw1map  16073  pwle2  16076  subctctexmid  16078  peano4nninf  16084  nninfalllem1  16086  nninfsellemdc  16088  nninfsellemeq  16092  nninfsellemqall  16093  nninfsellemeqinf  16094  isomninnlem  16110  trilpolemlt1  16121  trirec0  16124  iswomninnlem  16129  iswomni0  16131  ismkvnnlem  16132  dceqnconst  16140  dcapnconst  16141