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  5365  fnresdisj  5369  fnimadisj  5379  fnimaeq0  5380  sbcfng  5406  foeq1  5477  foco  5492  fveqeq2d  5567  fvelimab  5618  fvun1  5628  fvmptdv2  5652  fneqeql  5671  dffo3  5710  fvsng  5759  fconstfvm  5781  eufnfv  5794  f1veqaeq  5817  dff13f  5818  f1elima  5821  foeqcnvco  5838  f1eqcocnv  5839  acexmidlemab  5917  ovanraleqv  5947  eloprabga  6010  ovmpodv2  6057  ovi3  6061  ovelimab  6075  caovcang  6086  caovcan  6089  caovimo  6118  suppssfv  6132  suppssov1  6133  caofinvl  6161  uchoice  6196  op1stg  6209  op2ndg  6210  eqop  6236  reldm  6245  xporderlem  6290  tposfo2  6326  frec0g  6456  freccllem  6461  frecfcllem  6463  frecsuclem  6465  frecsuc  6466  nnm0r  6538  nnmord  6576  nnaordex  6587  nnawordex  6588  ereq1  6600  eqerlem  6624  mapsn  6750  endisj  6884  pw2f1odclem  6896  xpf1o  6906  mapxpen  6910  fidifsnen  6932  supelti  7069  updjudhcoinlf  7147  updjudhcoinrg  7148  updjud  7149  omp1eomlem  7161  difinfsnlem  7166  nnnninfeq  7195  enomnilem  7205  finomni  7207  exmidomni  7209  fodjuomnilemres  7215  fodjuomni  7216  ismkvnex  7222  mkvprop  7225  fodjumkvlemres  7226  enmkvlem  7228  enwomnilem  7236  nninfdcinf  7238  nninfwlporlem  7240  nninfwlpoimlemginf  7243  pm54.43  7259  exmidfodomrlemrALT  7272  cc2lem  7335  addnidpig  7405  ltexpi  7406  dfplpq2  7423  dfmpq2  7424  recexnq  7459  recmulnqg  7460  ltexnqq  7477  halfnqq  7479  enq0tr  7503  nqnq0pi  7507  addnnnq0  7518  addlocpr  7605  ltexprlemru  7681  ltexpri  7682  lteupri  7686  prplnqu  7689  recexpr  7707  addsrpr  7814  mulsrpr  7815  00sr  7838  negexsr  7841  recexgt0sr  7842  srpospr  7852  prsrriota  7857  caucvgsrlemfv  7860  map2psrprg  7874  elrealeu  7898  axrnegex  7948  axprecex  7949  rereceu  7958  recriota  7959  nntopi  7963  axcaucvglemval  7966  axcaucvglemcau  7967  cnegexlem1  8203  cnegex  8206  cnegex2  8207  subval  8220  subadd  8231  subadd2  8232  subsub23  8233  addsubeq4  8243  subcan2  8253  negcon1  8280  subcan  8283  addrsub  8399  ltadd2  8448  ltordlem  8511  recexre  8607  recexap  8682  muleqadd  8697  receuap  8698  divvalap  8703  divmulap  8704  rec11ap  8739  rerecapb  8872  zdiv  9416  uzin  9636  xaddval  9922  xnn0xadd0  9944  xnegdi  9945  xltadd1  9953  icc0r  10003  fznlem  10118  fseq1m1p1  10172  1fv  10216  fzon  10244  fvinim0ffz  10319  ioo0  10351  ico0  10353  ioc0  10354  flqbi  10382  divfl0  10388  modq0  10423  modqmuladdnn0  10462  addmodlteq  10492  frecuzrdgtcl  10506  frecuzrdgfunlem  10513  seq3f1olemstep  10608  seq3f1olemp  10609  seq3id  10619  seq3z  10622  qsqeqor  10744  mulreap  11031  rennim  11169  resqrexlemex  11192  rsqrmo  11194  resqrtcl  11196  rersqrtthlem  11197  sqrtsq2  11210  isumss  11558  fsum00  11629  telfsumo  11633  pwm1geoserap1  11675  prodssdc  11756  absefib  11938  efieq1re  11939  divides  11956  dvdsval2  11957  nndivides  11964  dvds0lem  11968  dvds1lem  11969  dvds2lem  11970  negdvdsb  11974  muldvds1  11983  muldvds2  11984  dvdscmulr  11987  dvdsmulcr  11988  dvdstr  11995  dvdsabseq  12014  divconjdvds  12016  odd2np1lem  12039  odd2np1  12040  even2n  12041  oddm1even  12042  2tp1odd  12051  opeo  12064  omeo  12065  m1exp1  12068  divalgb  12092  gcdaddm  12161  gcdabs1  12166  bezout  12188  gcdmultiple  12197  gcdmultiplez  12198  rplpwr  12204  rppwr  12205  nninfctlemfo  12217  alginv  12225  algcvga  12229  algfx  12230  eucalgval2  12231  coprmdvds  12270  qredeq  12274  qredeu  12275  divgcdcoprm0  12279  divgcdcoprmex  12280  cncongr1  12281  rpexp  12331  rpexp12i  12333  cncongrprm  12335  qnumdenbi  12370  phival  12391  phicl2  12392  dfphi2  12398  phiprmpw  12400  phimullem  12403  eulerthlem1  12405  eulerthlemfi  12406  eulerthlemrprm  12407  eulerthlemth  12410  eulerth  12411  fermltl  12412  hashgcdlem  12416  phisum  12419  odzval  12420  odzdvds  12424  reumodprminv  12432  modprm0  12433  nnnn0modprm0  12434  modprmn0modprm0  12435  coprimeprodsq  12436  coprimeprodsq2  12437  pythagtriplem2  12445  pythagtrip  12462  pceulem  12473  pcval  12475  pcqmul  12482  pcqcl  12485  pcabs  12505  pc2dvds  12509  pcaddlem  12518  pcadd  12519  pcmpt  12522  prmpwdvds  12534  pockthi  12537  4sqlem12  12581  ennnfonelemhf1o  12640  fvprif  12996  mgmidmo  13025  grpidvalg  13026  grpidpropdg  13027  ismgmid  13030  ismgmid2  13033  mgmidsssn0  13037  grpinvalem  13038  grprida  13040  igsumvalx  13042  gsumress  13048  ismnddef  13069  sgrpidmndm  13071  ismndd  13088  mndpropd  13091  mndinvmod  13096  mnd1  13097  ismhm  13103  gsumvallem2  13135  grpinvex  13152  isgrpd2  13163  isgrpd  13165  dfgrp2  13169  grpinveu  13180  grpinvval  13185  grplinv  13192  isgrpinv  13196  grplrinv  13199  grpidinv2  13200  grpidinv  13201  grplmulf1o  13216  grpsubeq0  13228  grpsubadd  13230  dfgrp3mlem  13240  dfgrp3m  13241  grp1  13248  imasgrp2  13250  qusgrp2  13253  mhmmnd  13256  ghmgrp  13258  mulgval  13262  mulgaddcom  13286  eqg0el  13369  ghmeqker  13411  ghmf1  13413  conjnmzb  13420  ablsubadd  13452  ablsubsub23  13465  rngmneg1  13513  rngmneg2  13514  dfur2g  13528  srgideu  13538  srgidmlem  13544  issrgid  13547  srgrz  13550  srglz  13551  srgisid  13552  srg1zr  13553  ringideu  13583  ringidmlem  13588  isringid  13591  ringid  13592  qusring2  13632  oppr0g  13647  oppr1g  13648  reldvdsrsrg  13658  dvdsrvald  13659  dvdsrmuld  13662  dvdsr01  13670  dvdsr02  13671  opprunitd  13676  crngunit  13677  unitinvinv  13690  dvreq1  13708  dvdsrpropdg  13713  rhmdvdsr  13741  lringuplu  13762  subrg1  13797  subrgdvds  13801  isrrg  13829  rrgeq0i  13830  rrgeq0  13831  domneq0  13838  islmod  13857  islmodd  13859  lmodprop2d  13914  lss1d  13949  cnfldui  14155  znval  14202  znidom  14223  znunit  14225  znrrg  14226  ntreq0  14378  ispsmet  14569  psmet0  14573  ismet  14590  isxmet  14591  xmeteq0  14605  metn0  14624  xmetres2  14625  xblss2ps  14650  xblss2  14651  xmseq0  14714  comet  14745  bdxmet  14747  cnmet  14776  ivthdec  14890  ivthreinc  14891  elply2  14981  reeff1o  15019  ioocosf1o  15100  logbgcd1irr  15213  logbgcd1irraplemexp  15214  mpodvdsmulf1o  15236  lgsval  15255  lgsdir  15286  lgsne0  15289  lgsprme0  15293  lgsdirnn0  15298  gausslemma2dlem0c  15302  gausslemma2dlem0i  15308  gausslemma2dlem7  15319  gausslemma2d  15320  lgseisenlem2  15322  lgseisenlem3  15323  lgsquadlem1  15328  lgsquadlem2  15329  lgsquad2lem2  15333  lgsquad3  15335  m1lgs  15336  2lgs  15355  2sqlem7  15372  2sqlem8  15374  2sqlem9  15375  bj-charfunbi  15467  pwle2  15653  subctctexmid  15655  peano4nninf  15660  nninfalllem1  15662  nninfsellemdc  15664  nninfsellemeq  15668  nninfsellemqall  15669  nninfsellemeqinf  15670  isomninnlem  15684  trilpolemlt1  15695  trirec0  15698  iswomninnlem  15703  iswomni0  15705  ismkvnnlem  15706  dceqnconst  15714  dcapnconst  15715