Theorem eqeq1i 2440

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

Hypothesis

Ref	Expression
eqeq1i.1	|- A = B

Assertion

Ref	Expression
eqeq1i	|- ( A = C <-> B = C )

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 |- A = B
2		eqeq1 2439	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	ax-mp 5	1 |- ( A = C <-> B = C )

Syntax hints:   <-> wb 184   = wceq 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426

This theorem is referenced by:  ssequn2  3517  dfss1  3543  dfss4  3572  disj  3707  disjr  3708  undisj1  3718  undisj2  3719  undif  3747  uneqdifeq  3755  reusn  3936  rabsneu  3938  eusn  3939  tppreqb  4002  uniintsn  4153  iin0  4454  opeqsn  4575  dfepfr  4692  epfrc  4693  unisuc  4782  dmopab3  5039  dm0rn0  5043  ssdmres  5120  imadisj  5176  args  5185  dffr3  5189  intirr  5204  dminxp  5266  dfrel3  5283  fntpg  5461  fncnv  5470  sbcfng  5544  dff1o4  5637  dffv4  5676  fvun2  5751  fnreseql  5801  riota1  6059  riota2df  6061  fnotovb  6118  ovid  6196  ov  6199  ovg  6218  ovima0  6231  opiota  6622  tz7.49c  6887  sucprcreg  7802  sucprcregOLD  7803  inf3lem2  7823  zfregs2  7941  rankxpsuc  8077  scott0s  8083  cplem1  8084  cfslb2n  8425  fin23lem26  8482  dfacfin7  8556  axdc3lem4  8610  zorn2lem7  8659  alephom  8737  fpwwe2  8798  recmulnq  9121  recexsr  9262  map2psrpr  9265  renegcli  9658  elznn0  10649  xrsupss  11259  xrinfmss  11260  seqf1olem1  11829  seqf1olem2  11830  sqeqori  11962  hashprb  12141  hash2pwpr  12166  hashbclem  12189  swrdccat3a  12369  f1oun2prg  12511  cshwrepswhash1  14112  ismgmid  15418  oppgid  15851  lsmdisjr  16161  gexex  16315  dprd0  16502  oppr1  16660  opprunit  16687  opprdomn  17295  iinopn  18357  elcls  18519  ordthaus  18830  hauscmplem  18851  regr1lem2  19155  metdseq0  20272  minveclem1  20753  minveclem3b  20757  volun  20868  dyaddisj  20918  vieta1  21663  logeftb  21917  birthdaylem1  22230  lgseisenlem1  22573  rpvmasum  22660  axsegconlem6  22991  usgraedgprv  23118  wlkdvspthlem  23329  rngosn3  23736  nmlno0lem  24016  minvecolem1  24098  hvsubeq0i  24288  hvsubaddi  24291  pjoc2i  24664  pjoml3i  24812  cmbr3i  24826  pjss2i  24906  hosubeq0i  25053  dmadjrnb  25133  nmlnop0iALT  25222  nmopcoadj0i  25330  stm1ri  25471  jplem2  25496  atoml2i  25610  chirredlem1  25617  cdj3lem3  25665  disjnf  25740  disjpreima  25752  disjunsn  25760  mptfnf  25800  f1od2  25848  addeq0  25860  zrhchr  26259  ddemeas  26506  braew  26512  aean  26514  eulerpartlemgh  26609  fib5  26636  fib6  26637  ballotlemfp1  26722  dmgmaddn0  26857  cvmsss2  27011  cvmlift2lem13  27052  elrn3  27420  br1steq  27432  br2ndeq  27433  sspred  27480  dffr4  27490  tz6.26  27513  wfi  27515  frind  27551  wfrlem8  27578  sltsolem1  27656  rankeq1o  28056  hfun  28063  tan2h  28268  asindmre  28323  totbndbnd  28532  scott0f  28826  coeq0  28935  fnresfnco  29878  afvpcfv0  29898  aovpcov0  29942  aov0ov0  29945  aovov0bi  29948  fnotaovb  29950  f0rn0  29987  hashrabsn1  30079  modfsummods  30090  wlknwwlknsur  30190  wlkiswwlksur  30197  clwlkfclwwlk1hashn  30360  clwlkfoclwwlk  30364  1to3vfriswmgra  30445  frgrawopreg2  30490  mat0dimcrng  30655  snlindsntor  30735  zfregs2VD  31300  bnj1143  31507  bj-pinftynminfty  32151  atbase  32528  llnbase  32747  lplnbase  32772  lvolbase  32816  lhpbase  33236  cdlemg31b0N  33932  cdlemg31b0a  33933  cdlemh  34055