Theorem eqeq1i 1479

Description: Inference from equality to equivalence of equalities.

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 1478	. 2 |- (A = B -> (A = C <-> B = C))
3	1, 2	ax-mp 7	1 |- (A = C <-> B = C)

Syntax hints:   <-> wb 146   = wceq 954

This theorem is referenced by:  eqeq12i 1485  ssequn2 2199  sseqin2 2225  dfss4 2238  disj 2307  undisj1 2316  undisj2 2317  undif 2339  iin0 2735  opeqsn 2797  reuuni1 2877  reusn 2887  dfepfr 2927  epfrc 2928  unisuc 3041  dmopab3 3317  dm0rn0 3325  dmxp 3327  ssdmres 3373  imadisj 3414  args 3420  dffr3 3423  dminxp 3475  dfrel3 3481  fncnv 3553  f1o4 3687  f1ocnv 3692  fvopab3ig 3769  fopab2 3814  tz7.44-2 3920  tz7.49c 3951  oprabval 4014  oprabvalig 4015  oprssdm 4033  map0 4334  pw2en 4432  mapunen 4488  zfreg2 4577  sucprcreg 4580  inf3lem2 4594  rankeq0 4676  rankxpsuc 4695  scott0s 4699  cplem1 4700  zorn2lem7 4774  recexsr 5196  map2psrpr 5200  supsrlem2 5206  subadd 5351  subadd2 5353  subsub23 5354  neg11 5386  negcon1 5387  renegcl 5396  lesubadd 5577  divmul 5682  xrsupss 6033  xrinfmss 6034  elznn0 6104  zltp1let 6136  sq00 6554  sqeqor 6586  sqr2irrlem1 6662  crulem 6674  negreb 6738  abs00 6785  cvgcmpub 7129  geoser 7177  ivth2OLD 7242  eirrlem5 7342  elcls 7654  islp2 7697  qdensere 7701  metne0 7773  lpbl 7832  bcthlem9 7957  nmlno0lem 8398  logeftb 8703  hvsubeq0 8869  hvsubadd 8872  pjoc2 9209  pjoml3 9469  cmbr3 9483  nonbool 9536  pjss2 9565  hosubeq0 9692  dmadjrnb 9770  nmlnop0ALT 9858  nmcopexlem1 9889  nmcfnexlem1 9918  nmopcoadj0 9974  pj3lem1 10072  stm1r 10109  jplem2 10134  atoml2 10247  irredlem1 10254  cdj3lem3 10299  oprabvaligg 10377  efilcp 10481  efilcp2 10486  homib 10604

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain