Theorem eqtr 1493

Description: An equality transitivity inference.

Hypotheses

Ref	Expression
eqtr.1	|- A = B
eqtr.2	|- B = C

Assertion

Ref	Expression
eqtr	|- A = C

Proof of Theorem eqtr

Step	Hyp	Ref	Expression
1		eqtr.1	. 2 |- A = B
2		eqtr.2	. . 3 |- B = C
3	2	eqeq2i 1483	. 2 |- (A = B <-> A = C)
4	1, 3	mpbi 189	1 |- A = C

Syntax hints:   = wceq 955

This theorem is referenced by:  eqtr2 1494  eqtr3 1495  eqtr4 1496  3eqtr 1497  3eqtr2 1499  3eqtr3 1501  3eqtr4 1503  rabab 1819  difeq12i 2154  dfun3 2243  dfin3 2244  invdif 2246  difundi 2254  difindi 2256  symdif1 2262  undif1 2337  dfif2 2360  dfpr2 2419  dfuni2 2501  intab 2556  intunsn 2561  unopab 2675  op1stb 2909  dfepfr 2928  orddif 3071  onuninsuc 3104  fconstopab 3206  onnev 3238  dfdm3 3298  dfrn3 3300  dmopab 3316  dmopab3 3318  dmxpin 3330  rnopab 3349  rncoss 3360  rncoeq 3363  resundi 3374  resopab 3391  dfima3 3402  imadisj 3418  ndmima 3430  op1sta 3444  op2ndb 3447  op2nda 3448  rnun 3453  imaun 3456  rnxp 3468  dminxp 3479  rescnvcnv 3489  resdmres 3493  cocnvcnv1 3501  cores2 3503  funi 3541  funcnvuni 3560  funcnvres 3564  fnresdisj 3593  fv2 3715  dfimafn2 3757  fvopab4gf 3776  fvsnun1 3790  abrexexlem2 3854  tfrlem3 3908  tfrlem9 3914  tfrlem10 3915  tz7.44-2 3924  dfrdg2 3928  rdglem1 3932  rdgsucopabn 3942  abianfplem 3956  opreq12i 3968  resoprab 4004  oprabval 4018  oprabvalig 4019  oprabval2gf 4021  oprabval5 4024  caopr31 4057  caopr42 4061  caoprdilem 4063  caoprmo 4065  op1st 4078  op2nd 4079  f1stres 4086  f2ndres 4087  curry1 4091  unielxp 4100  dfopab2 4106  dfoprab3 4107  dfoprab5 4108  df1o2 4133  ecidsn 4280  oprec 4311  fnmap 4322  mapvalg 4323  pmvalg 4324  map0 4337  xpassen 4430  sbthlem5 4440  sbthlem8 4443  fodomr 4472  mapunen 4491  ssenen 4493  limensuci 4495  phplem1 4497  abfii4 4547  abfii5 4548  pm54.43 4555  supex 4560  inf3lema 4592  inf3lemb 4593  trcl 4628  zfregs 4630  r10 4634  rankval 4651  rankuni 4681  ranksuc 4683  rankxpu 4694  rankxplim3 4697  rankxpsuc 4698  kardex 4708  hta 4711  aceq3 4716  ac6lem 4737  kmlem11 4758  kmlem12 4759  zorn2lem1 4771  brdom7disj 4787  brdom6disj 4788  aleph0 4846  alephfplem1 4879  cf0 4893  cdavalt 4902  cdaassen 4913  addpiord 4995  mulpiord 4996  dmaddpi 5001  dmmulpi 5002  addcmpblnq 5035  addcompq 5045  dmrecpq 5057  ltapq 5059  ltmpq 5060  1lt2pq 5061  ltaddpq 5062  mulcomsr 5181  distrsr 5183  ltasr 5192  recexsrlem 5195  sqgt0sr 5198  map2psrpr 5203  supsrlem4 5211  supsrlem5 5212  addcnsr 5236  mulcnsr 5237  mulresr 5240  axmulcom 5259  axmulass 5261  axdistr 5262  axi2m1 5268  axcnre 5269  mulid2 5316  add42 5326  negsub 5364  neg0 5398  mul02 5415  1p1times 5416  mul2neg 5430  negdi 5431  mnfnre 5480  renfdisj 5522  ssxr 5523  ltsubadd 5578  divcan1 5696  divrec 5710  divcan3 5724  divcan4 5725  divid 5736  recgt0i 5780  2times 5960  2t2e4 5979  3t2e6 5980  3t3e9 5981  4t2e8 5982  5t2e10 5983  8th4div3 5988  halfpm6th 5989  infmsup 6025  nneo 6154  uzwo3lem2 6175  om2uz0 6245  uzrdgini 6253  seq1lem1 6259  seq1rval 6261  ser11 6285  shftidt 6305  dfioo2 6349  icoshftf1oi 6355  uzinfm 6407  nninfm 6408  nn0infm 6409  seq1seq0t 6489  seq00 6495  ser00 6511  sqreci 6564  sumsqne0 6579  sq2 6583  sq3 6584  cu2 6585  binom2 6589  binom2aOLD 6590  discrlem1 6601  nn0opthlem1 6609  sqrlem10 6627  sqrlem11 6628  sqrlem16 6633  sqrth 6644  sqr2irrlem1 6669  i2 6677  i3 6678  crne0 6685  cjcj 6728  recj 6732  imcj 6733  readd 6734  imadd 6735  remul 6736  immul 6737  cjadd 6738  reneg 6744  imneg 6746  cjneg 6747  cji 6777  absval2 6791  abs00 6792  absmul 6797  absid 6811  abstri 6844  fac0 6886  fac1 6887  facp1t 6888  fac2 6889  faclbnd4lem1 6900  faclbnd4lem4 6903  bcpasc2 6920  sumeq12i 6942  serzfsum 6957  csbfsumlem 6979  dfisum 7144  isumnn0nna 7160  isum0split 7169  fnsmntlem 7177  geoser 7186  geolim1i 7190  0.999... 7198  fsum0diag 7210  fsum0diag2 7211  ivthlem6 7238  ivthlem7 7239  dsupivthlem 7243  ivthlem6OLD 7247  ivthlem7OLD 7248  ef0lem 7269  efseq0ex 7270  efcvgfsum 7274  erelem2 7279  erelem6 7283  ele3lem 7285  ege2le3lem2 7288  efaddlem5 7301  efaddlem8 7304  efaddlem20 7316  efaddlem22 7318  ef1tllem 7340  eirrlem1 7347  eirrlem2 7348  efsep 7354  ef4p 7357  reeff1 7367  efm1lim 7368  sin0 7403  cos0 7405  sinadd 7410  cosadd 7411  cos1bnd 7433  cos2bnd 7434  acdc3lem 7445  acdc3 7446  acdc2 7449  acdc5 7452  acdc 7454  ruclem2 7471  ruclem3 7472  ruclem14 7483  ruclem15 7484  infxpidmlem6 7517  infxpidmlem11 7522  infmap2lem1 7539  subbas2 7605  subtop 7606  indistop 7608  fctop 7610  cctop 7612  uniretop 7617  cnco 7728  dfms2 7759  metssba 7769  cnmetdval 7864  cnmetba 7865  cncfmet 7867  cncfmet1 7868  remetdval 7870  oprcn 7939  bcthlem9 7969  issubg 8080  grpsn 8088  ringsn 8127  vcm 8154  vcnegneg 8157  vafval 8186  smfval 8188  nmfval 8190  nvnncan 8247  nvm1 8256  nvpi 8258  nvmtri 8263  cnnvg 8272  cnnvs 8275  abscn 8305  ipval2lem1 8313  ipval2 8319  ipid 8325  ip0r 8332  nmblolbii 8418  blocnilem 8423  ip2i 8446  ipdirilem 8447  ipasslem10 8458  siilem1 8470  siii 8472  minvecex 8537  spwval2 8610  pilem1 8625  pilem3 8627  sinhalfpilem 8633  cospi 8636  eulerid 8637  sin2pi 8638  cos2pi 8639  sinperlem1 8640  sincosq4sgn 8659  sincos4thpi 8662  sincos6thpi 8663  cosh111lem1 8664  effoi 8700  pilog 8723  grothprim 8738  avril1 8739  hvsubass 8877  hvnegdi 8884  hvsubeq0 8885  hvsubcan2 8886  normlem0 8930  normlem1 8931  normlem9 8939  normsq 8954  norm-ii 8959  norm-iii 8961  normsub 8963  normpar 8976  normpar2 8978  polid2 8979  bcsALT 9001  hhssva 9084  hhsssm 9085  hhssnv 9089  hhshsslem1 9092  hhsssh2 9095  projlem3 9143  projlem4 9144  projlem7 9147  projlem18 9158  pjthlem1 9174  ococ 9202  dfchsup2 9253  dfchj2 9279  dfchj3 9280  chdmm2 9356  chdmm3 9357  chdmm4 9358  chdmj2 9360  chdmj3 9361  chdmj4 9362  chjo 9366  h1de2 9431  spanunsn 9459  pjoml3 9486  pjoml4 9487  cmbr2 9496  cmbr3 9500  qlax5 9529  qlaxr2 9531  osumcor2 9547  pjadj 9575  pjadd 9577  pjmul 9579  pjsub 9580  pjssm 9583  pjdifnorm 9585  pjcj 9586  pjpyth 9624  dfiop2 9636  hoid1 9672  hoid1r 9673  honegnegt 9689  hosd1 9705  hosubeq0 9709  ho01 9711  dfadj2 9769  cnvadj 9773  adj1o 9775  dmadjss 9776  hhlno 9783  hh0o 9786  lnop0t 9847  nmop0h 9872  lnopunilem1 9891  lnophmlem2 9898  nmbdoplb 9905  lnfn0 9927  cnlnadjlem5 9960  adjbdlnt 9972  nmoptri2 9988  kbass2t 10006  kbass5t 10009  mdsl1 10204  cvmd 10207  mdsldmd1 10214  mdslmd3 10215  mdexch 10218  shatomistic 10244  cvexch 10252  atord 10267  sumdmdlem2 10302  ghomgrpilem2 10342  ghomgrp 10346  symgval 10359  symggrpi 10362  symgidi 10363  cayleylem3 10367  oprabvaligg 10399  fopab2ga 10419  fopab2a 10420  dmhmph 10478  rnhmph 10479  subsp 10488  domval 10571  codval 10572  idval 10573  cmpval 10574  1ded 10587  1cat 10608  dmo 10625  cmpmorp 10628  ishomb 10632  mrdmcd 10638  homib 10640  cmphmia 10642  cmphmib 10643  iri 10644  idmon 10660

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

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

Copyright terms: Public domain