Theorem eqeq1i 2770

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq1i	⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq1 2769	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 197   = wceq 1652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758

This theorem is referenced by:  eqeq12i  2779  neeq1i  3001  ssequn2  3950  sseqin2  3981  dfss4  4025  rabeq0  4123  disj  4180  disjr  4181  undisj1  4192  undisj2  4193  undif  4211  uneqdifeq  4219  rabeqsn  4373  reusn  4419  rabsneu  4421  eusn  4422  tppreqb  4492  elpreqpr  4555  uniintsn  4672  iin0  4999  opeqsnOLD  5126  dfepfr  5264  epfrc  5265  dmopab3  5507  dm0rn0  5512  ssdmres  5597  imadisj  5668  args  5677  dffr3  5682  intirr  5699  dminxp  5759  dfrel3  5777  coeq0  5832  sspred  5875  dffr4  5883  tz6.26  5898  wfi  5900  unisuc  5986  fntpg  6129  fncnv  6142  mptfnf  6195  sbcfng  6222  f0rn0  6274  dff1o4  6330  dffv4  6374  fvun2  6461  fnreseql  6519  funopdmsn  6609  riota1  6823  riota2df  6825  riotaeqimp  6828  fnbrovb  6892  fnotovbOLD  6894  ovid  6977  ov  6980  ovg  6999  ovima0  7013  opiota  7431  wfrlem8  7628  tz7.49c  7747  sucprcreg  8715  zfregfr  8718  inf3lem2  8743  zfregs2  8826  rankxpsuc  8962  scott0s  8968  cplem1  8969  cfslb2n  9345  fin23lem26  9402  dfacfin7  9476  axdc3lem4  9530  zorn2lem7  9579  alephom  9662  fpwwe2  9720  recmulnq  10041  recexsr  10183  map2psrpr  10186  renegcli  10598  elznn0  11641  xrsupss  12344  xrinfmss  12345  prinfzo0  12718  seqf1olem1  13050  seqf1olem2  13051  sqeqori  13186  hashrabsn1  13368  hashprb  13389  hashprdifel  13390  hashbclem  13440  hash2pwpr  13462  swrdccat3aOLD  13751  f1oun2prg  13949  modfsummods  14812  cshwrepswhash1  16086  ismgmid  17533  oppgid  18052  lsmdisjr  18364  gexex  18525  dprd0  18700  oppr1  18904  opprunit  18931  opprdomn  19578  gsummoncoe1  19950  zringndrg  20114  mat0dimcrng  20556  iinopn  20989  elcls  21160  ordthaus  21471  hauscmplem  21492  regr1lem2  21826  metdseq0  22939  minveclem1  23487  minveclem3b  23491  volun  23606  dyaddisj  23657  vieta1  24361  logeftb  24624  birthdaylem1  24972  dmgmaddn0  25043  gausslemma2d  25393  lgseisenlem1  25394  2lgslem4  25425  rpvmasum  25509  axsegconlem6  26096  edg0iedg0  26229  numedglnl  26320  ushgredgedg  26402  ushgredgedgloop  26404  ushgredgedgloopOLD  26405  uhgr0v0e  26412  usgr1v0edg  26431  usgrexmpllem  26434  usgr1v0e  26500  nbuhgr2vtx1edgblem  26529  uvtx01vtx  26584  uvtxa01vtx0OLD  26586  prcliscplgr  26603  cusgr0v  26618  vtxdg0e  26664  1loopgrvd2  26693  finsumvtxdg2ssteplem4  26738  finsumvtxdg2size  26740  isrgr  26749  fusgrregdegfi  26759  wlknwwlksnsurOLD  27085  wlkwwlksurOLD  27093  wspn0  27150  2wlkdlem8  27159  clwlksfclwwlk1hashnOLD  27337  clwlksfoclwwlkOLD  27341  3wlkdlem8  27448  uhgr3cyclexlem  27462  1to2vfriswmgr  27562  1to3vfriswmgr  27563  frgrregorufr0  27607  frgrreg  27713  frgrregord013  27714  ex-ceil  27767  nmlno0lem  28107  minvecolem1  28189  hvsubeq0i  28379  hvsubaddi  28382  pjoc2i  28756  pjoml3i  28904  cmbr3i  28918  pjss2i  28998  hosubeq0i  29144  dmadjrnb  29224  nmlnop0iALT  29313  nmopcoadj0i  29421  stm1ri  29562  jplem2  29587  atoml2i  29701  chirredlem1  29708  cdj3lem3  29756  difininv  29806  disjnf  29835  disjpreima  29848  disjunsn  29858  f1od2  29951  addeq0  29962  zrhchr  30470  ddemeas  30749  braew  30755  aean  30757  eulerpartlemgh  30890  ballotlemfp1  31004  repr0  31143  hgt750lem2  31184  bnj1143  31312  cvmsss2  31707  cvmlift2lem13  31748  elrn3  32100  frpomin2  32186  frpoind  32187  frind  32190  sltsolem1  32273  madeval2  32383  rankeq1o  32725  hfun  32732  bj-disj2r  33443  bj-sscon  33444  bj-0int  33486  bj-pinftynminfty  33551  finxpreclem4  33667  curunc  33818  tan2h  33828  poimirlem13  33849  poimirlem14  33850  poimirlem21  33857  poimirlem22  33858  asindmre  33921  totbndbnd  34013  rngosn3  34148  scott0f  34401  ineqcom  34445  n0el2  34535  dfrel5  34546  dfrel6  34547  redeq1  34802  atbase  35248  llnbase  35468  lplnbase  35493  lvolbase  35537  lhpbase  35957  cdlemg31b0N  36653  cdlemg31b0a  36654  cdlemh  36776  iunrelexp0  38672  frege120  38954  clsk1indlem4  39019  gneispace  39109  undisjrab  39182  zfregs2VD  39732  dvnprod  40805  fnresfnco  41821  aiotavb  41836  afvpcfv0  41897  aovpcov0  41941  aov0ov0  41944  aovov0bi  41947  fnotaovb  41949  funressndmafv2rn  41974  dfss7  42029  fmtnoprmfac1lem  42155  lighneallem2  42202  snlindsntor  42932