Theorem eqeq1i 1485

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

Syntax hints:   <-> wb 146   = wceq 958

This theorem is referenced by:  eqeq12i 1491  ssequn2 2206  sseqin2 2232  dfss4 2245  disj 2315  undisj1 2324  undisj2 2325  undif 2347  iin0 2745  opeqsn 2808  reuuni1 2888  reusn 2898  dfepfr 2938  epfrc 2939  unisuc 3052  dmopab3 3328  dm0rn0 3336  dmxp 3338  ssdmres 3387  imadisj 3428  args 3434  dffr3 3437  dminxp 3489  dfrel3 3495  fncnv 3567  f1o4 3702  f1ocnv 3707  fvopab3ig 3784  fopab2 3829  tz7.44-2 3935  tz7.49c 3966  oprabval 4029  oprabvalig 4030  oprssdm 4048  map0 4350  pw2en 4452  mapunen 4508  zfreg2 4606  sucprcreg 4609  inf3lem2 4623  rankeq0 4706  rankxpsuc 4725  scott0s 4729  cplem1 4730  zorn2lem7 4804  recexsr 5228  map2psrpr 5232  supsrlem2 5238  subadd 5383  subadd2 5385  subsub23 5386  neg11 5418  negcon1 5419  renegcl 5428  lesubadd 5607  divmul 5717  xrsupss 6080  xrinfmss 6081  elznn0 6151  zltp1let 6183  sqeqor 6648  sqr2irrlem1 6725  crulem 6737  negreb 6795  abs00 6842  cvgcmpub 7185  geoser 7234  eirrlem5 7393  elcls 7701  islp2 7744  qdensere 7748  metne0 7818  lpbl 7877  bcthlem9 8004  nmlno0lem 8449  logeftb 8759  hvsubeq0 8925  hvsubadd 8928  pjoc2 9266  pjoml3 9524  cmbr3 9538  nonbool 9591  pjss2 9620  hosubeq0 9747  dmadjrnb 9825  nmlnop0ALT 9915  nmcopexlem1 9946  nmcfnexlem1 9975  nmopcoadj0 10031  pj3lem1 10129  stm1r 10166  jplem2 10191  atoml2 10305  irredlem1 10312  cdj3lem3 10360  oprabvaligg 10435  efilcp 10556  efilcp2 10561  homib 10695

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain