Theorem eqeq1d 2240

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  rspcedeq1vd  2919  sbceq2g  3149  csbhypf  3166  csbiebt  3167  csbiebg  3170  dfss4st  3440  disjssun  3558  sneqrg  3845  preq12b  3853  preq12bg  3856  disji2  4080  invdisjrab  4082  iin0r  4259  opthg  4330  opeqsn  4345  unisucg  4511  opthreg  4654  tfisi  4685  dmsnopg  5208  relcoi1  5268  iotaeq  5295  iotabi  5296  fneq1  5418  fnun  5438  fnresdisj  5442  fnimadisj  5453  fnimaeq0  5454  sbcfng  5480  foeq1  5555  foco  5570  fveqeq2d  5647  fvelimab  5702  fvun1  5712  fvmptdv2  5736  fneqeql  5755  dffo3  5794  fvsng  5850  fconstfvm  5872  eufnfv  5885  f1veqaeq  5910  dff13f  5911  f1elima  5914  foeqcnvco  5931  f1eqcocnv  5932  acexmidlemab  6012  ovanraleqv  6042  eloprabga  6108  ovmpodv2  6155  ovi3  6159  ovelimab  6173  caovcang  6184  caovcan  6187  caovimo  6216  suppssfv  6231  suppssov1  6232  caofinvl  6261  caofid1  6264  caofid2  6265  uchoice  6300  op1stg  6313  op2ndg  6314  eqop  6340  reldm  6349  xporderlem  6396  tposfo2  6433  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnm0r  6647  nnmord  6685  nnaordex  6696  nnawordex  6697  ereq1  6709  eqerlem  6733  mapsn  6859  endisj  7008  pw2f1odclem  7020  xpf1o  7030  mapxpen  7034  fidifsnen  7057  supelti  7201  updjudhcoinlf  7279  updjudhcoinrg  7280  updjud  7281  omp1eomlem  7293  difinfsnlem  7298  nnnninfeq  7327  enomnilem  7337  finomni  7339  exmidomni  7341  fodjuomnilemres  7347  fodjuomni  7348  ismkvnex  7354  mkvprop  7357  fodjumkvlemres  7358  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemginf  7375  pm54.43  7395  exmidfodomrlemrALT  7414  cc2lem  7485  addnidpig  7556  ltexpi  7557  dfplpq2  7574  dfmpq2  7575  recexnq  7610  recmulnqg  7611  ltexnqq  7628  halfnqq  7630  enq0tr  7654  nqnq0pi  7658  addnnnq0  7669  addlocpr  7756  ltexprlemru  7832  ltexpri  7833  lteupri  7837  prplnqu  7840  recexpr  7858  addsrpr  7965  mulsrpr  7966  00sr  7989  negexsr  7992  recexgt0sr  7993  srpospr  8003  prsrriota  8008  caucvgsrlemfv  8011  map2psrprg  8025  elrealeu  8049  axrnegex  8099  axprecex  8100  rereceu  8109  recriota  8110  nntopi  8114  axcaucvglemval  8117  axcaucvglemcau  8118  cnegexlem1  8354  cnegex  8357  cnegex2  8358  subval  8371  subadd  8382  subadd2  8383  subsub23  8384  addsubeq4  8394  subcan2  8404  negcon1  8431  subcan  8434  addrsub  8550  ltadd2  8599  ltordlem  8662  recexre  8758  recexap  8833  muleqadd  8848  receuap  8849  divvalap  8854  divmulap  8855  rec11ap  8890  rerecapb  9023  zdiv  9568  uzin  9789  xaddval  10080  xnn0xadd0  10102  xnegdi  10103  xltadd1  10111  icc0r  10161  fznlem  10276  fseq1m1p1  10330  1fv  10374  fzon  10402  fvinim0ffz  10488  ioo0  10520  ico0  10522  ioc0  10523  flqbi  10551  divfl0  10557  modq0  10592  modqmuladdnn0  10631  addmodlteq  10661  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seq3f1olemstep  10777  seq3f1olemp  10778  seq3id  10788  seq3z  10791  qsqeqor  10913  hashtpglem  11111  ccat0  11177  wrdl1s1  11211  ccatws1lenp1bg  11216  pfxsuff1eqwrdeq  11284  swrdccatin2  11314  pfxccatin12lem2  11316  mulreap  11429  rennim  11567  resqrexlemex  11590  rsqrmo  11592  resqrtcl  11594  rersqrtthlem  11595  sqrtsq2  11608  isumss  11957  fsum00  12028  telfsumo  12032  pwm1geoserap1  12074  prodssdc  12155  absefib  12337  efieq1re  12338  divides  12355  dvdsval2  12356  nndivides  12363  dvds0lem  12367  dvds1lem  12368  dvds2lem  12369  negdvdsb  12373  muldvds1  12382  muldvds2  12383  dvdscmulr  12386  dvdsmulcr  12387  dvdstr  12394  dvdsabseq  12413  divconjdvds  12415  odd2np1lem  12438  odd2np1  12439  even2n  12440  oddm1even  12441  2tp1odd  12450  opeo  12463  omeo  12464  m1exp1  12467  divalgb  12491  gcdaddm  12560  gcdabs1  12565  bezout  12587  gcdmultiple  12596  gcdmultiplez  12597  rplpwr  12603  rppwr  12604  nninfctlemfo  12616  alginv  12624  algcvga  12628  algfx  12629  eucalgval2  12630  coprmdvds  12669  qredeq  12673  qredeu  12674  divgcdcoprm0  12678  divgcdcoprmex  12679  cncongr1  12680  rpexp  12730  rpexp12i  12732  cncongrprm  12734  qnumdenbi  12769  phival  12790  phicl2  12791  dfphi2  12797  phiprmpw  12799  phimullem  12802  eulerthlem1  12804  eulerthlemfi  12805  eulerthlemrprm  12806  eulerthlemth  12809  eulerth  12810  fermltl  12811  hashgcdlem  12815  phisum  12818  odzval  12819  odzdvds  12823  reumodprminv  12831  modprm0  12832  nnnn0modprm0  12833  modprmn0modprm0  12834  coprimeprodsq  12835  coprimeprodsq2  12836  pythagtriplem2  12844  pythagtrip  12861  pceulem  12872  pcval  12874  pcqmul  12881  pcqcl  12884  pcabs  12904  pc2dvds  12908  pcaddlem  12917  pcadd  12918  pcmpt  12921  prmpwdvds  12933  pockthi  12936  4sqlem12  12980  ennnfonelemhf1o  13039  fvprif  13431  mgmidmo  13460  grpidvalg  13461  grpidpropdg  13462  ismgmid  13465  ismgmid2  13468  mgmidsssn0  13472  grpinvalem  13473  grprida  13475  igsumvalx  13477  gsumress  13483  ismnddef  13506  sgrpidmndm  13508  ismndd  13525  mndpropd  13528  mndinvmod  13533  mnd1  13543  ismhm  13549  gsumvallem2  13581  grpinvex  13598  isgrpd2  13609  isgrpd  13611  dfgrp2  13615  grpinveu  13626  grpinvval  13631  grplinv  13638  isgrpinv  13642  grplrinv  13645  grpidinv2  13646  grpidinv  13647  grplmulf1o  13662  grpsubeq0  13674  grpsubadd  13676  dfgrp3mlem  13686  dfgrp3m  13687  grp1  13694  imasgrp2  13702  qusgrp2  13705  mhmmnd  13708  ghmgrp  13710  mulgval  13714  mulgaddcom  13738  eqg0el  13821  ghmeqker  13863  ghmf1  13865  conjnmzb  13872  ablsubadd  13904  ablsubsub23  13917  rngmneg1  13966  rngmneg2  13967  dfur2g  13981  srgideu  13991  srgidmlem  13997  issrgid  14000  srgrz  14003  srglz  14004  srgisid  14005  srg1zr  14006  ringideu  14036  ringidmlem  14041  isringid  14044  ringid  14045  qusring2  14085  oppr0g  14100  oppr1g  14101  dvdsrvald  14113  dvdsrmuld  14116  dvdsr01  14124  dvdsr02  14125  opprunitd  14130  crngunit  14131  unitinvinv  14144  dvreq1  14162  dvdsrpropdg  14167  rhmdvdsr  14195  lringuplu  14216  subrg1  14251  subrgdvds  14255  isrrg  14283  rrgeq0i  14284  rrgeq0  14285  domneq0  14292  islmod  14311  islmodd  14313  lmodprop2d  14368  lss1d  14403  cnfldui  14609  znval  14656  znidom  14677  znunit  14679  znrrg  14680  mplelbascoe  14712  ntreq0  14862  ispsmet  15053  psmet0  15057  ismet  15074  isxmet  15075  xmeteq0  15089  metn0  15108  xmetres2  15109  xblss2ps  15134  xblss2  15135  xmseq0  15198  comet  15229  bdxmet  15231  cnmet  15260  ivthdec  15374  ivthreinc  15375  elply2  15465  reeff1o  15503  ioocosf1o  15584  logbgcd1irr  15697  logbgcd1irraplemexp  15698  mpodvdsmulf1o  15720  lgsval  15739  lgsdir  15770  lgsne0  15773  lgsprme0  15777  lgsdirnn0  15782  gausslemma2dlem0c  15786  gausslemma2dlem0i  15792  gausslemma2dlem7  15803  gausslemma2d  15804  lgseisenlem2  15806  lgseisenlem3  15807  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem2  15817  lgsquad3  15819  m1lgs  15820  2lgs  15839  2sqlem7  15856  2sqlem8  15858  2sqlem9  15859  edg0iedg0g  15923  upgredg  16001  ushgredgedgloop  16085  edg0usgr  16104  vtxdgfval  16145  vtxdgop  16149  vtxdeqd  16153  vtxdfifiun  16154  vtxd0nedgbfi  16156  1loopgrvd2fi  16162  wksfval  16179  wlklenvclwlk  16230  clwwlknon  16286  isclwwlknon  16287  s2elclwwlknon2  16293  depind  16354  bj-charfunbi  16432  2omap  16620  pw1map  16622  pwle2  16625  subctctexmid  16627  peano4nninf  16634  nninfalllem1  16636  nninfsellemdc  16638  nninfsellemeq  16642  nninfsellemqall  16643  nninfsellemeqinf  16644  isomninnlem  16660  trilpolemlt1  16671  trirec0  16674  qdiff  16679  iswomninnlem  16680  iswomni0  16682  ismkvnnlem  16683  dceqnconst  16691  dcapnconst  16692