Theorem eqeq1d 2247

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  rspcedeq1vd  2939  sbceq2g  3169  csbhypf  3186  csbiebt  3187  csbiebg  3190  dfss4st  3464  disjssun  3588  sneqrg  3887  preq12b  3895  preq12bg  3898  disji2  4122  invdisjrab  4124  iin0r  4308  opthg  4380  opeqsn  4395  unisucg  4561  opthreg  4705  tfisi  4736  dmsnopg  5262  relcoi1  5322  iotaeq  5349  iotabi  5350  fneq1  5472  fnun  5492  fnresdisj  5496  fnimadisj  5507  fnimaeq0  5508  sbcfng  5534  foeq1  5614  foco  5629  fveqeq2d  5706  fvelimab  5762  fvun1  5772  fvmptdv2  5798  fneqeql  5820  dffo3  5858  fvsng  5914  fconstfvm  5936  eufnfv  5952  f1veqaeq  5978  dff13f  5979  f1elima  5982  foeqcnvco  5999  f1eqcocnv  6000  acexmidlemab  6082  ovanraleqv  6112  eloprabga  6178  ovmpodv2  6225  ovi3  6229  ovelimab  6243  caovcang  6254  caovcan  6257  caovimo  6286  suppssov1  6302  caofinvl  6332  caofid1  6335  caofid2  6336  uchoice  6375  op1stg  6388  op2ndg  6389  eqop  6415  reldm  6424  xporderlem  6471  suppofss1dcl  6508  suppofss2dcl  6509  tposfo2  6543  frec0g  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  nnm0r  6757  nnmord  6795  nnaordex  6806  nnawordex  6807  ereq1  6819  eqerlem  6843  mapsnd  6976  mapsn  6978  endisj  7128  pw2f1odclem  7140  xpf1o  7150  mapxpen  7154  fidifsnen  7178  2omap  7324  supelti  7348  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  omp1eomlem  7440  difinfsnlem  7445  nnnninfeq  7474  enomnilem  7484  finomni  7486  exmidomni  7488  fodjuomnilemres  7494  fodjuomni  7495  ismkvnex  7501  mkvprop  7504  fodjumkvlemres  7505  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemginf  7522  pm54.43  7542  exmidfodomrlemrALT  7561  cc2lem  7638  addnidpig  7709  ltexpi  7710  dfplpq2  7727  dfmpq2  7728  recexnq  7763  recmulnqg  7764  ltexnqq  7781  halfnqq  7783  enq0tr  7807  nqnq0pi  7811  addnnnq0  7822  addlocpr  7909  ltexprlemru  7985  ltexpri  7986  lteupri  7990  prplnqu  7993  recexpr  8011  addsrpr  8118  mulsrpr  8119  00sr  8142  negexsr  8145  recexgt0sr  8146  srpospr  8156  prsrriota  8161  caucvgsrlemfv  8164  map2psrprg  8178  elrealeu  8202  axrnegex  8252  axprecex  8253  rereceu  8262  recriota  8263  nntopi  8267  axcaucvglemval  8270  axcaucvglemcau  8271  cnegexlem1  8508  cnegex  8511  cnegex2  8512  subval  8525  subadd  8536  subadd2  8537  subsub23  8538  addsubeq4  8548  subcan2  8558  negcon1  8585  subcan  8588  addrsub  8704  ltadd2  8754  ltordlem  8817  recexre  8914  recexap  8989  muleqadd  9006  receuap  9007  divvalap  9012  divmulap  9013  rec11ap  9048  rerecapb  9181  zdiv  9744  uzin  9970  xaddval  10263  xnn0xadd0  10285  xnegdi  10286  xltadd1  10294  icc0r  10344  fznlem  10461  fseq1m1p1  10518  1fv  10562  fzon  10590  fvinim0ffz  10676  ioo0  10710  ico0  10712  ioc0  10713  flqbi  10745  divfl0  10751  modq0  10786  modqmuladdnn0  10825  addmodlteq  10855  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  seq3f1olemstep  10971  seq3f1olemp  10972  seq3id  10982  seq3z  10985  qsqeqor  11107  hashfibc  11304  hashf1lem1  11306  hashtpglem  11319  ccat0  11385  wrdl1s1  11419  ccatws1lenp1bg  11424  pfxsuff1eqwrdeq  11492  swrdccatin2  11522  pfxccatin12lem2  11524  mulreap  11650  rennim  11789  resqrexlemex  11812  rsqrmo  11814  resqrtcl  11816  rersqrtthlem  11817  sqrtsq2  11830  isumss  12182  fsum00  12253  telfsumo  12257  pwm1geoserap1  12299  prodssdc  12380  absefib  12562  efieq1re  12563  divides  12580  dvdsval2  12581  nndivides  12588  dvds0lem  12592  dvds1lem  12593  dvds2lem  12594  negdvdsb  12598  muldvds1  12607  muldvds2  12608  dvdscmulr  12611  dvdsmulcr  12612  dvdstr  12619  dvdsabseq  12638  divconjdvds  12640  odd2np1lem  12663  odd2np1  12664  even2n  12665  oddm1even  12666  2tp1odd  12675  opeo  12688  omeo  12689  m1exp1  12692  divalgb  12716  gcdaddm  12785  gcdabs1  12790  bezout  12812  gcdmultiple  12821  gcdmultiplez  12822  rplpwr  12828  rppwr  12829  nninfctlemfo  12841  alginv  12849  algcvga  12853  algfx  12854  eucalgval2  12855  coprmdvds  12894  qredeq  12898  qredeu  12899  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  rpexp  12956  rpexp12i  12958  cncongrprm  12960  qnumdenbi  12996  phival  13019  phicl2  13020  dfphi2  13026  phiprmpw  13028  phimullem  13031  eulerthlem1  13033  eulerthlemfi  13034  eulerthlemrprm  13035  eulerthlemth  13038  eulerth  13039  fermltl  13040  hashgcdlem  13044  phisum  13047  odzval  13048  odzdvds  13052  reumodprminv  13060  modprm0  13061  nnnn0modprm0  13062  modprmn0modprm0  13063  coprimeprodsq  13064  coprimeprodsq2  13065  pythagtriplem2  13073  pythagtrip  13090  pceulem  13101  pcval  13103  pcqmul  13110  pcqcl  13113  pcabs  13133  pc2dvds  13137  pcaddlem  13146  pcadd  13147  pcmpt  13150  prmpwdvds  13162  pockthi  13165  4sqlem12  13209  ballotfilemi  13300  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemsima  13316  ballotfilemfrcn0  13330  ballotfi  13339  ennnfonelemhf1o  13361  fvprif  13722  mgmidmo  13750  grpidvalg  13751  grpidpropdg  13752  ismgmid  13755  ismgmid2  13758  mgmidsssn0  13762  grpinvalem  13763  grprida  13765  gzsumvalx  13767  gzsumress  13770  ismnddef  13789  sgrpidmndm  13791  ismndd  13808  mndpropd  13811  mndinvmod  13816  mnd1  13820  ismhm  13826  gsumvallem2  13858  grpinvex  13873  isgrpd2  13884  isgrpd  13886  dfgrp2  13890  grpinveu  13901  grpinvval  13906  grplinv  13913  isgrpinv  13917  grplrinv  13920  grpidinv2  13921  grpidinv  13922  grplmulf1o  13937  grpsubeq0  13949  grpsubadd  13951  dfgrp3mlem  13961  dfgrp3m  13962  grp1  13969  imasgrp2  13971  qusgrp2  13974  mhmmnd  13977  ghmgrp  13979  mulgval  13983  mulgaddcom  14007  eqg0el  14090  ghmeqker  14132  ghmf1  14134  conjnmzb  14141  ablsubadd  14205  ablsubsub23  14218  gsumzfi  14247  gsumsnfdcmn  14256  rngmneg1  14352  rngmneg2  14353  rng1zrlem  14364  dfur2g  14372  srgideu  14382  srgidmlem  14388  issrgid  14391  srgrz  14394  srglz  14395  srgisid  14396  ringideu  14427  ringidmlem  14433  isringid  14436  ringid  14437  qusring2  14479  oppr0g  14495  oppr1g  14496  dvdsrvald  14508  dvdsrmuld  14511  dvdsr01  14519  dvdsr02  14520  opprunitd  14525  crngunit  14526  unitinvinv  14539  dvreq1  14557  dvdsrpropdg  14562  rhmdvdsr  14590  lringuplu  14611  subrg1  14647  subrgdvds  14651  isrrg  14679  rrgeq0i  14680  rrgeq0  14681  domneq0  14689  islmod  14735  islmodd  14737  lmodprop2d  14793  lss1d  14828  cnfldui  15032  znval  15079  znidom  15100  znunit  15102  znrrg  15103  psrlidmfi  15208  psrridmfi  15209  ntreq0  15375  ispsmet  15566  psmet0  15570  ismet  15587  isxmet  15588  xmeteq0  15602  metn0  15621  xmetres2  15622  xblss2ps  15647  xblss2  15648  xmseq0  15711  comet  15742  bdxmet  15744  cnmet  15773  ivthdec  15887  ivthreinc  15888  elply2  15978  reeff1o  16016  sineq0re  16093  ioocosf1o  16099  efnthr  16193  logbgcd1irr  16220  logbgcd1irraplemexp  16221  birthdaylem1g  16242  mpodvdsmulf1o  16301  ppiqub  16310  lgsval  16345  lgsdir  16376  lgsne0  16379  lgsprme0  16383  lgsdirnn0  16388  gausslemma2dlem0c  16392  gausslemma2dlem0i  16398  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem2  16412  lgseisenlem3  16413  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  lgsquad3  16425  m1lgs  16426  2lgs  16445  2sqlem7  16462  2sqlem8  16464  2sqlem9  16465  edg0iedg0g  16529  upgredg  16607  ushgredgedgloop  16691  edg0usgr  16710  vtxdgfval  16751  vtxdgop  16755  vtxdeqd  16759  vtxdfifiun  16760  vtxd0nedgbfi  16762  1loopgrvd2fi  16768  wksfval  16785  wlklenvclwlk  16836  clwwlknon  16892  isclwwlknon  16893  s2elclwwlknon2  16899  depind  16972  dichmul0orlem7  16981  bj-charfunbi  17059  pw1map  17247  pwle2  17250  subctctexmid  17252  wexmiddifxylem  17267  peano4nninf  17272  nninfalllem1  17274  nninfsellemdc  17276  nninfsellemeq  17280  nninfsellemqall  17281  nninfsellemeqinf  17282  isomninnlem  17302  trilpolemlt1  17314  trirec0  17317  qdiff  17322  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  dceqnconst  17334  dcapnconst  17335