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  5849  fconstfvm  5871  eufnfv  5884  f1veqaeq  5909  dff13f  5910  f1elima  5913  foeqcnvco  5930  f1eqcocnv  5931  acexmidlemab  6011  ovanraleqv  6041  eloprabga  6107  ovmpodv2  6154  ovi3  6158  ovelimab  6172  caovcang  6183  caovcan  6186  caovimo  6215  suppssfv  6230  suppssov1  6231  caofinvl  6260  caofid1  6263  caofid2  6264  uchoice  6299  op1stg  6312  op2ndg  6313  eqop  6339  reldm  6348  xporderlem  6395  tposfo2  6432  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  nnm0r  6646  nnmord  6684  nnaordex  6695  nnawordex  6696  ereq1  6708  eqerlem  6732  mapsn  6858  endisj  7007  pw2f1odclem  7019  xpf1o  7029  mapxpen  7033  fidifsnen  7056  supelti  7200  updjudhcoinlf  7278  updjudhcoinrg  7279  updjud  7280  omp1eomlem  7292  difinfsnlem  7297  nnnninfeq  7326  enomnilem  7336  finomni  7338  exmidomni  7340  fodjuomnilemres  7346  fodjuomni  7347  ismkvnex  7353  mkvprop  7356  fodjumkvlemres  7357  enmkvlem  7359  enwomnilem  7367  nninfdcinf  7369  nninfwlporlem  7371  nninfwlpoimlemginf  7374  pm54.43  7394  exmidfodomrlemrALT  7413  cc2lem  7484  addnidpig  7555  ltexpi  7556  dfplpq2  7573  dfmpq2  7574  recexnq  7609  recmulnqg  7610  ltexnqq  7627  halfnqq  7629  enq0tr  7653  nqnq0pi  7657  addnnnq0  7668  addlocpr  7755  ltexprlemru  7831  ltexpri  7832  lteupri  7836  prplnqu  7839  recexpr  7857  addsrpr  7964  mulsrpr  7965  00sr  7988  negexsr  7991  recexgt0sr  7992  srpospr  8002  prsrriota  8007  caucvgsrlemfv  8010  map2psrprg  8024  elrealeu  8048  axrnegex  8098  axprecex  8099  rereceu  8108  recriota  8109  nntopi  8113  axcaucvglemval  8116  axcaucvglemcau  8117  cnegexlem1  8353  cnegex  8356  cnegex2  8357  subval  8370  subadd  8381  subadd2  8382  subsub23  8383  addsubeq4  8393  subcan2  8403  negcon1  8430  subcan  8433  addrsub  8549  ltadd2  8598  ltordlem  8661  recexre  8757  recexap  8832  muleqadd  8847  receuap  8848  divvalap  8853  divmulap  8854  rec11ap  8889  rerecapb  9022  zdiv  9567  uzin  9788  xaddval  10079  xnn0xadd0  10101  xnegdi  10102  xltadd1  10110  icc0r  10160  fznlem  10275  fseq1m1p1  10329  1fv  10373  fzon  10401  fvinim0ffz  10486  ioo0  10518  ico0  10520  ioc0  10521  flqbi  10549  divfl0  10555  modq0  10590  modqmuladdnn0  10629  addmodlteq  10659  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  seq3f1olemstep  10775  seq3f1olemp  10776  seq3id  10786  seq3z  10789  qsqeqor  10911  ccat0  11172  wrdl1s1  11206  ccatws1lenp1bg  11211  pfxsuff1eqwrdeq  11279  swrdccatin2  11309  pfxccatin12lem2  11311  mulreap  11424  rennim  11562  resqrexlemex  11585  rsqrmo  11587  resqrtcl  11589  rersqrtthlem  11590  sqrtsq2  11603  isumss  11951  fsum00  12022  telfsumo  12026  pwm1geoserap1  12068  prodssdc  12149  absefib  12331  efieq1re  12332  divides  12349  dvdsval2  12350  nndivides  12357  dvds0lem  12361  dvds1lem  12362  dvds2lem  12363  negdvdsb  12367  muldvds1  12376  muldvds2  12377  dvdscmulr  12380  dvdsmulcr  12381  dvdstr  12388  dvdsabseq  12407  divconjdvds  12409  odd2np1lem  12432  odd2np1  12433  even2n  12434  oddm1even  12435  2tp1odd  12444  opeo  12457  omeo  12458  m1exp1  12461  divalgb  12485  gcdaddm  12554  gcdabs1  12559  bezout  12581  gcdmultiple  12590  gcdmultiplez  12591  rplpwr  12597  rppwr  12598  nninfctlemfo  12610  alginv  12618  algcvga  12622  algfx  12623  eucalgval2  12624  coprmdvds  12663  qredeq  12667  qredeu  12668  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  rpexp  12724  rpexp12i  12726  cncongrprm  12728  qnumdenbi  12763  phival  12784  phicl2  12785  dfphi2  12791  phiprmpw  12793  phimullem  12796  eulerthlem1  12798  eulerthlemfi  12799  eulerthlemrprm  12800  eulerthlemth  12803  eulerth  12804  fermltl  12805  hashgcdlem  12809  phisum  12812  odzval  12813  odzdvds  12817  reumodprminv  12825  modprm0  12826  nnnn0modprm0  12827  modprmn0modprm0  12828  coprimeprodsq  12829  coprimeprodsq2  12830  pythagtriplem2  12838  pythagtrip  12855  pceulem  12866  pcval  12868  pcqmul  12875  pcqcl  12878  pcabs  12898  pc2dvds  12902  pcaddlem  12911  pcadd  12912  pcmpt  12915  prmpwdvds  12927  pockthi  12930  4sqlem12  12974  ennnfonelemhf1o  13033  fvprif  13425  mgmidmo  13454  grpidvalg  13455  grpidpropdg  13456  ismgmid  13459  ismgmid2  13462  mgmidsssn0  13466  grpinvalem  13467  grprida  13469  igsumvalx  13471  gsumress  13477  ismnddef  13500  sgrpidmndm  13502  ismndd  13519  mndpropd  13522  mndinvmod  13527  mnd1  13537  ismhm  13543  gsumvallem2  13575  grpinvex  13592  isgrpd2  13603  isgrpd  13605  dfgrp2  13609  grpinveu  13620  grpinvval  13625  grplinv  13632  isgrpinv  13636  grplrinv  13639  grpidinv2  13640  grpidinv  13641  grplmulf1o  13656  grpsubeq0  13668  grpsubadd  13670  dfgrp3mlem  13680  dfgrp3m  13681  grp1  13688  imasgrp2  13696  qusgrp2  13699  mhmmnd  13702  ghmgrp  13704  mulgval  13708  mulgaddcom  13732  eqg0el  13815  ghmeqker  13857  ghmf1  13859  conjnmzb  13866  ablsubadd  13898  ablsubsub23  13911  rngmneg1  13959  rngmneg2  13960  dfur2g  13974  srgideu  13984  srgidmlem  13990  issrgid  13993  srgrz  13996  srglz  13997  srgisid  13998  srg1zr  13999  ringideu  14029  ringidmlem  14034  isringid  14037  ringid  14038  qusring2  14078  oppr0g  14093  oppr1g  14094  dvdsrvald  14106  dvdsrmuld  14109  dvdsr01  14117  dvdsr02  14118  opprunitd  14123  crngunit  14124  unitinvinv  14137  dvreq1  14155  dvdsrpropdg  14160  rhmdvdsr  14188  lringuplu  14209  subrg1  14244  subrgdvds  14248  isrrg  14276  rrgeq0i  14277  rrgeq0  14278  domneq0  14285  islmod  14304  islmodd  14306  lmodprop2d  14361  lss1d  14396  cnfldui  14602  znval  14649  znidom  14670  znunit  14672  znrrg  14673  mplelbascoe  14705  ntreq0  14855  ispsmet  15046  psmet0  15050  ismet  15067  isxmet  15068  xmeteq0  15082  metn0  15101  xmetres2  15102  xblss2ps  15127  xblss2  15128  xmseq0  15191  comet  15222  bdxmet  15224  cnmet  15253  ivthdec  15367  ivthreinc  15368  elply2  15458  reeff1o  15496  ioocosf1o  15577  logbgcd1irr  15690  logbgcd1irraplemexp  15691  mpodvdsmulf1o  15713  lgsval  15732  lgsdir  15763  lgsne0  15766  lgsprme0  15770  lgsdirnn0  15775  gausslemma2dlem0c  15779  gausslemma2dlem0i  15785  gausslemma2dlem7  15796  gausslemma2d  15797  lgseisenlem2  15799  lgseisenlem3  15800  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  lgsquad3  15812  m1lgs  15813  2lgs  15832  2sqlem7  15849  2sqlem8  15851  2sqlem9  15852  edg0iedg0g  15916  upgredg  15994  ushgredgedgloop  16078  edg0usgr  16097  vtxdgfval  16138  vtxdgop  16142  vtxdeqd  16146  vtxdfifiun  16147  vtxd0nedgbfi  16149  1loopgrvd2fi  16155  wksfval  16172  wlklenvclwlk  16223  clwwlknon  16279  isclwwlknon  16280  s2elclwwlknon2  16286  bj-charfunbi  16406  2omap  16594  pw1map  16596  pwle2  16599  subctctexmid  16601  peano4nninf  16608  nninfalllem1  16610  nninfsellemdc  16612  nninfsellemeq  16616  nninfsellemqall  16617  nninfsellemeqinf  16618  isomninnlem  16634  trilpolemlt1  16645  trirec0  16648  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  dceqnconst  16664  dcapnconst  16665