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  4306  opthg  4378  opeqsn  4393  unisucg  4559  opthreg  4703  tfisi  4734  dmsnopg  5259  relcoi1  5319  iotaeq  5346  iotabi  5347  fneq1  5469  fnun  5489  fnresdisj  5493  fnimadisj  5504  fnimaeq0  5505  sbcfng  5531  foeq1  5611  foco  5626  fveqeq2d  5703  fvelimab  5759  fvun1  5769  fvmptdv2  5795  fneqeql  5817  dffo3  5855  fvsng  5911  fconstfvm  5933  eufnfv  5949  f1veqaeq  5975  dff13f  5976  f1elima  5979  foeqcnvco  5996  f1eqcocnv  5997  acexmidlemab  6079  ovanraleqv  6109  eloprabga  6175  ovmpodv2  6222  ovi3  6226  ovelimab  6240  caovcang  6251  caovcan  6254  caovimo  6283  suppssov1  6299  caofinvl  6328  caofid1  6331  caofid2  6332  uchoice  6371  op1stg  6384  op2ndg  6385  eqop  6411  reldm  6420  xporderlem  6467  suppofss1dcl  6504  suppofss2dcl  6505  tposfo2  6538  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnm0r  6752  nnmord  6790  nnaordex  6801  nnawordex  6802  ereq1  6814  eqerlem  6838  mapsnd  6970  mapsn  6972  endisj  7122  pw2f1odclem  7134  xpf1o  7144  mapxpen  7148  fidifsnen  7172  2omap  7318  supelti  7342  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  omp1eomlem  7434  difinfsnlem  7439  nnnninfeq  7468  enomnilem  7478  finomni  7480  exmidomni  7482  fodjuomnilemres  7488  fodjuomni  7489  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemginf  7516  pm54.43  7536  exmidfodomrlemrALT  7555  cc2lem  7632  addnidpig  7703  ltexpi  7704  dfplpq2  7721  dfmpq2  7722  recexnq  7757  recmulnqg  7758  ltexnqq  7775  halfnqq  7777  enq0tr  7801  nqnq0pi  7805  addnnnq0  7816  addlocpr  7903  ltexprlemru  7979  ltexpri  7980  lteupri  7984  prplnqu  7987  recexpr  8005  addsrpr  8112  mulsrpr  8113  00sr  8136  negexsr  8139  recexgt0sr  8140  srpospr  8150  prsrriota  8155  caucvgsrlemfv  8158  map2psrprg  8172  elrealeu  8196  axrnegex  8246  axprecex  8247  rereceu  8256  recriota  8257  nntopi  8261  axcaucvglemval  8264  axcaucvglemcau  8265  cnegexlem1  8501  cnegex  8504  cnegex2  8505  subval  8518  subadd  8529  subadd2  8530  subsub23  8531  addsubeq4  8541  subcan2  8551  negcon1  8578  subcan  8581  addrsub  8697  ltadd2  8747  ltordlem  8810  recexre  8906  recexap  8981  muleqadd  8998  receuap  8999  divvalap  9004  divmulap  9005  rec11ap  9040  rerecapb  9173  zdiv  9734  uzin  9955  xaddval  10247  xnn0xadd0  10269  xnegdi  10270  xltadd1  10278  icc0r  10328  fznlem  10445  fseq1m1p1  10502  1fv  10546  fzon  10574  fvinim0ffz  10660  ioo0  10694  ico0  10696  ioc0  10697  flqbi  10725  divfl0  10731  modq0  10766  modqmuladdnn0  10805  addmodlteq  10835  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  seq3f1olemstep  10951  seq3f1olemp  10952  seq3id  10962  seq3z  10965  qsqeqor  11087  hashfibc  11283  hashf1lem1  11285  hashtpglem  11298  ccat0  11364  wrdl1s1  11398  ccatws1lenp1bg  11403  pfxsuff1eqwrdeq  11471  swrdccatin2  11501  pfxccatin12lem2  11503  mulreap  11629  rennim  11768  resqrexlemex  11791  rsqrmo  11793  resqrtcl  11795  rersqrtthlem  11796  sqrtsq2  11809  isumss  12158  fsum00  12229  telfsumo  12233  pwm1geoserap1  12275  prodssdc  12356  absefib  12538  efieq1re  12539  divides  12556  dvdsval2  12557  nndivides  12564  dvds0lem  12568  dvds1lem  12569  dvds2lem  12570  negdvdsb  12574  muldvds1  12583  muldvds2  12584  dvdscmulr  12587  dvdsmulcr  12588  dvdstr  12595  dvdsabseq  12614  divconjdvds  12616  odd2np1lem  12639  odd2np1  12640  even2n  12641  oddm1even  12642  2tp1odd  12651  opeo  12664  omeo  12665  m1exp1  12668  divalgb  12692  gcdaddm  12761  gcdabs1  12766  bezout  12788  gcdmultiple  12797  gcdmultiplez  12798  rplpwr  12804  rppwr  12805  nninfctlemfo  12817  alginv  12825  algcvga  12829  algfx  12830  eucalgval2  12831  coprmdvds  12870  qredeq  12874  qredeu  12875  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  rpexp  12931  rpexp12i  12933  cncongrprm  12935  qnumdenbi  12970  phival  12991  phicl2  12992  dfphi2  12998  phiprmpw  13000  phimullem  13003  eulerthlem1  13005  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlemth  13010  eulerth  13011  fermltl  13012  hashgcdlem  13016  phisum  13019  odzval  13020  odzdvds  13024  reumodprminv  13032  modprm0  13033  nnnn0modprm0  13034  modprmn0modprm0  13035  coprimeprodsq  13036  coprimeprodsq2  13037  pythagtriplem2  13045  pythagtrip  13062  pceulem  13073  pcval  13075  pcqmul  13082  pcqcl  13085  pcabs  13105  pc2dvds  13109  pcaddlem  13118  pcadd  13119  pcmpt  13122  prmpwdvds  13134  pockthi  13137  4sqlem12  13181  ballotfilemi  13243  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemsima  13259  ballotfilemfrcn0  13273  ballotfi  13282  ennnfonelemhf1o  13304  fvprif  13664  mgmidmo  13692  grpidvalg  13693  grpidpropdg  13694  ismgmid  13697  ismgmid2  13700  mgmidsssn0  13704  grpinvalem  13705  grprida  13707  gzsumvalx  13709  gzsumress  13712  ismnddef  13731  sgrpidmndm  13733  ismndd  13750  mndpropd  13753  mndinvmod  13758  mnd1  13762  ismhm  13768  gsumvallem2  13800  grpinvex  13815  isgrpd2  13826  isgrpd  13828  dfgrp2  13832  grpinveu  13843  grpinvval  13848  grplinv  13855  isgrpinv  13859  grplrinv  13862  grpidinv2  13863  grpidinv  13864  grplmulf1o  13879  grpsubeq0  13891  grpsubadd  13893  dfgrp3mlem  13903  dfgrp3m  13904  grp1  13911  imasgrp2  13913  qusgrp2  13916  mhmmnd  13919  ghmgrp  13921  mulgval  13925  mulgaddcom  13949  eqg0el  14032  ghmeqker  14074  ghmf1  14076  conjnmzb  14083  ablsubadd  14116  ablsubsub23  14129  gsumzfi  14158  rngmneg1  14246  rngmneg2  14247  rng1zrlem  14258  dfur2g  14266  srgideu  14276  srgidmlem  14282  issrgid  14285  srgrz  14288  srglz  14289  srgisid  14290  ringideu  14321  ringidmlem  14327  isringid  14330  ringid  14331  qusring2  14371  oppr0g  14387  oppr1g  14388  dvdsrvald  14400  dvdsrmuld  14403  dvdsr01  14411  dvdsr02  14412  opprunitd  14417  crngunit  14418  unitinvinv  14431  dvreq1  14449  dvdsrpropdg  14454  rhmdvdsr  14482  lringuplu  14503  subrg1  14539  subrgdvds  14543  isrrg  14571  rrgeq0i  14572  rrgeq0  14573  domneq0  14581  islmod  14627  islmodd  14629  lmodprop2d  14685  lss1d  14720  cnfldui  14924  znval  14971  znidom  14992  znunit  14994  znrrg  14995  mplelbascoe  15083  ntreq0  15233  ispsmet  15424  psmet0  15428  ismet  15445  isxmet  15446  xmeteq0  15460  metn0  15479  xmetres2  15480  xblss2ps  15505  xblss2  15506  xmseq0  15569  comet  15600  bdxmet  15602  cnmet  15631  ivthdec  15745  ivthreinc  15746  elply2  15836  reeff1o  15874  ioocosf1o  15955  logbgcd1irr  16069  logbgcd1irraplemexp  16070  birthdaylem1g  16087  mpodvdsmulf1o  16104  lgsval  16123  lgsdir  16154  lgsne0  16157  lgsprme0  16161  lgsdirnn0  16166  gausslemma2dlem0c  16170  gausslemma2dlem0i  16176  gausslemma2dlem7  16187  gausslemma2d  16188  lgseisenlem2  16190  lgseisenlem3  16191  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  lgsquad3  16203  m1lgs  16204  2lgs  16223  2sqlem7  16240  2sqlem8  16242  2sqlem9  16243  edg0iedg0g  16307  upgredg  16385  ushgredgedgloop  16469  edg0usgr  16488  vtxdgfval  16529  vtxdgop  16533  vtxdeqd  16537  vtxdfifiun  16538  vtxd0nedgbfi  16540  1loopgrvd2fi  16546  wksfval  16563  wlklenvclwlk  16614  clwwlknon  16670  isclwwlknon  16671  s2elclwwlknon2  16677  depind  16750  dichmul0orlem7  16759  bj-charfunbi  16837  pw1map  17025  pwle2  17028  subctctexmid  17030  wexmiddifxylem  17045  peano4nninf  17049  nninfalllem1  17051  nninfsellemdc  17053  nninfsellemeq  17057  nninfsellemqall  17058  nninfsellemeqinf  17059  isomninnlem  17079  trilpolemlt1  17090  trirec0  17093  qdiff  17098  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  dceqnconst  17110  dcapnconst  17111