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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  rspcedeq1vd  2920  sbceq2g  3150  csbhypf  3167  csbiebt  3168  csbiebg  3171  dfss4st  3442  disjssun  3560  sneqrg  3850  preq12b  3858  preq12bg  3861  disji2  4085  invdisjrab  4087  iin0r  4265  opthg  4336  opeqsn  4351  unisucg  4517  opthreg  4660  tfisi  4691  dmsnopg  5215  relcoi1  5275  iotaeq  5302  iotabi  5303  fneq1  5425  fnun  5445  fnresdisj  5449  fnimadisj  5460  fnimaeq0  5461  sbcfng  5487  foeq1  5564  foco  5579  fveqeq2d  5656  fvelimab  5711  fvun1  5721  fvmptdv2  5745  fneqeql  5764  dffo3  5802  fvsng  5858  fconstfvm  5880  eufnfv  5895  f1veqaeq  5920  dff13f  5921  f1elima  5924  foeqcnvco  5941  f1eqcocnv  5942  acexmidlemab  6022  ovanraleqv  6052  eloprabga  6118  ovmpodv2  6165  ovi3  6169  ovelimab  6183  caovcang  6194  caovcan  6197  caovimo  6226  suppssov1  6241  caofinvl  6270  caofid1  6273  caofid2  6274  uchoice  6309  op1stg  6322  op2ndg  6323  eqop  6349  reldm  6358  xporderlem  6405  suppofss1dcl  6442  suppofss2dcl  6443  tposfo2  6476  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnm0r  6690  nnmord  6728  nnaordex  6739  nnawordex  6740  ereq1  6752  eqerlem  6776  mapsn  6902  endisj  7051  pw2f1odclem  7063  xpf1o  7073  mapxpen  7077  fidifsnen  7100  supelti  7244  updjudhcoinlf  7322  updjudhcoinrg  7323  updjud  7324  omp1eomlem  7336  difinfsnlem  7341  nnnninfeq  7370  enomnilem  7380  finomni  7382  exmidomni  7384  fodjuomnilemres  7390  fodjuomni  7391  ismkvnex  7397  mkvprop  7400  fodjumkvlemres  7401  enmkvlem  7403  enwomnilem  7411  nninfdcinf  7413  nninfwlporlem  7415  nninfwlpoimlemginf  7418  pm54.43  7438  exmidfodomrlemrALT  7457  cc2lem  7528  addnidpig  7599  ltexpi  7600  dfplpq2  7617  dfmpq2  7618  recexnq  7653  recmulnqg  7654  ltexnqq  7671  halfnqq  7673  enq0tr  7697  nqnq0pi  7701  addnnnq0  7712  addlocpr  7799  ltexprlemru  7875  ltexpri  7876  lteupri  7880  prplnqu  7883  recexpr  7901  addsrpr  8008  mulsrpr  8009  00sr  8032  negexsr  8035  recexgt0sr  8036  srpospr  8046  prsrriota  8051  caucvgsrlemfv  8054  map2psrprg  8068  elrealeu  8092  axrnegex  8142  axprecex  8143  rereceu  8152  recriota  8153  nntopi  8157  axcaucvglemval  8160  axcaucvglemcau  8161  cnegexlem1  8396  cnegex  8399  cnegex2  8400  subval  8413  subadd  8424  subadd2  8425  subsub23  8426  addsubeq4  8436  subcan2  8446  negcon1  8473  subcan  8476  addrsub  8592  ltadd2  8641  ltordlem  8704  recexre  8800  recexap  8875  muleqadd  8890  receuap  8891  divvalap  8896  divmulap  8897  rec11ap  8932  rerecapb  9065  zdiv  9612  uzin  9833  xaddval  10124  xnn0xadd0  10146  xnegdi  10147  xltadd1  10155  icc0r  10205  fznlem  10321  fseq1m1p1  10375  1fv  10419  fzon  10447  fvinim0ffz  10533  ioo0  10565  ico0  10567  ioc0  10568  flqbi  10596  divfl0  10602  modq0  10637  modqmuladdnn0  10676  addmodlteq  10706  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  seq3f1olemstep  10822  seq3f1olemp  10823  seq3id  10833  seq3z  10836  qsqeqor  10958  hashtpglem  11156  ccat0  11222  wrdl1s1  11256  ccatws1lenp1bg  11261  pfxsuff1eqwrdeq  11329  swrdccatin2  11359  pfxccatin12lem2  11361  mulreap  11487  rennim  11625  resqrexlemex  11648  rsqrmo  11650  resqrtcl  11652  rersqrtthlem  11653  sqrtsq2  11666  isumss  12015  fsum00  12086  telfsumo  12090  pwm1geoserap1  12132  prodssdc  12213  absefib  12395  efieq1re  12396  divides  12413  dvdsval2  12414  nndivides  12421  dvds0lem  12425  dvds1lem  12426  dvds2lem  12427  negdvdsb  12431  muldvds1  12440  muldvds2  12441  dvdscmulr  12444  dvdsmulcr  12445  dvdstr  12452  dvdsabseq  12471  divconjdvds  12473  odd2np1lem  12496  odd2np1  12497  even2n  12498  oddm1even  12499  2tp1odd  12508  opeo  12521  omeo  12522  m1exp1  12525  divalgb  12549  gcdaddm  12618  gcdabs1  12623  bezout  12645  gcdmultiple  12654  gcdmultiplez  12655  rplpwr  12661  rppwr  12662  nninfctlemfo  12674  alginv  12682  algcvga  12686  algfx  12687  eucalgval2  12688  coprmdvds  12727  qredeq  12731  qredeu  12732  divgcdcoprm0  12736  divgcdcoprmex  12737  cncongr1  12738  rpexp  12788  rpexp12i  12790  cncongrprm  12792  qnumdenbi  12827  phival  12848  phicl2  12849  dfphi2  12855  phiprmpw  12857  phimullem  12860  eulerthlem1  12862  eulerthlemfi  12863  eulerthlemrprm  12864  eulerthlemth  12867  eulerth  12868  fermltl  12869  hashgcdlem  12873  phisum  12876  odzval  12877  odzdvds  12881  reumodprminv  12889  modprm0  12890  nnnn0modprm0  12891  modprmn0modprm0  12892  coprimeprodsq  12893  coprimeprodsq2  12894  pythagtriplem2  12902  pythagtrip  12919  pceulem  12930  pcval  12932  pcqmul  12939  pcqcl  12942  pcabs  12962  pc2dvds  12966  pcaddlem  12975  pcadd  12976  pcmpt  12979  prmpwdvds  12991  pockthi  12994  4sqlem12  13038  ennnfonelemhf1o  13097  fvprif  13489  mgmidmo  13518  grpidvalg  13519  grpidpropdg  13520  ismgmid  13523  ismgmid2  13526  mgmidsssn0  13530  grpinvalem  13531  grprida  13533  igsumvalx  13535  gsumress  13541  ismnddef  13564  sgrpidmndm  13566  ismndd  13583  mndpropd  13586  mndinvmod  13591  mnd1  13601  ismhm  13607  gsumvallem2  13639  grpinvex  13656  isgrpd2  13667  isgrpd  13669  dfgrp2  13673  grpinveu  13684  grpinvval  13689  grplinv  13696  isgrpinv  13700  grplrinv  13703  grpidinv2  13704  grpidinv  13705  grplmulf1o  13720  grpsubeq0  13732  grpsubadd  13734  dfgrp3mlem  13744  dfgrp3m  13745  grp1  13752  imasgrp2  13760  qusgrp2  13763  mhmmnd  13766  ghmgrp  13768  mulgval  13772  mulgaddcom  13796  eqg0el  13879  ghmeqker  13921  ghmf1  13923  conjnmzb  13930  ablsubadd  13962  ablsubsub23  13975  rngmneg1  14024  rngmneg2  14025  dfur2g  14039  srgideu  14049  srgidmlem  14055  issrgid  14058  srgrz  14061  srglz  14062  srgisid  14063  srg1zr  14064  ringideu  14094  ringidmlem  14099  isringid  14102  ringid  14103  qusring2  14143  oppr0g  14158  oppr1g  14159  dvdsrvald  14171  dvdsrmuld  14174  dvdsr01  14182  dvdsr02  14183  opprunitd  14188  crngunit  14189  unitinvinv  14202  dvreq1  14220  dvdsrpropdg  14225  rhmdvdsr  14253  lringuplu  14274  subrg1  14309  subrgdvds  14313  isrrg  14341  rrgeq0i  14342  rrgeq0  14343  domneq0  14351  islmod  14370  islmodd  14372  lmodprop2d  14427  lss1d  14462  cnfldui  14668  znval  14715  znidom  14736  znunit  14738  znrrg  14739  mplelbascoe  14776  ntreq0  14926  ispsmet  15117  psmet0  15121  ismet  15138  isxmet  15139  xmeteq0  15153  metn0  15172  xmetres2  15173  xblss2ps  15198  xblss2  15199  xmseq0  15262  comet  15293  bdxmet  15295  cnmet  15324  ivthdec  15438  ivthreinc  15439  elply2  15529  reeff1o  15567  ioocosf1o  15648  logbgcd1irr  15761  logbgcd1irraplemexp  15762  mpodvdsmulf1o  15787  lgsval  15806  lgsdir  15837  lgsne0  15840  lgsprme0  15844  lgsdirnn0  15849  gausslemma2dlem0c  15853  gausslemma2dlem0i  15859  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem2  15873  lgseisenlem3  15874  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem2  15884  lgsquad3  15886  m1lgs  15887  2lgs  15906  2sqlem7  15923  2sqlem8  15925  2sqlem9  15926  edg0iedg0g  15990  upgredg  16068  ushgredgedgloop  16152  edg0usgr  16171  vtxdgfval  16212  vtxdgop  16216  vtxdeqd  16220  vtxdfifiun  16221  vtxd0nedgbfi  16223  1loopgrvd2fi  16229  wksfval  16246  wlklenvclwlk  16297  clwwlknon  16353  isclwwlknon  16354  s2elclwwlknon2  16360  depind  16433  bj-charfunbi  16510  2omap  16698  pw1map  16700  pwle2  16703  subctctexmid  16705  peano4nninf  16715  nninfalllem1  16717  nninfsellemdc  16719  nninfsellemeq  16723  nninfsellemqall  16724  nninfsellemeqinf  16725  isomninnlem  16745  trilpolemlt1  16756  trirec0  16759  qdiff  16764  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768  dceqnconst  16776  dcapnconst  16777