Theorem eqtri 1908

Description: An equality transitivity inference.

Hypotheses

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

Assertion

Ref	Expression
eqtri	|- A = C

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 |- A = B
2		eqtri.2	. . 3 |- B = C
3	2	eqeq2i 1894	. 2 |- (A = B <-> A = C)
4	1, 3	mpbi 206	1 |- A = C

Syntax hints:   = wceq 1298

This theorem is referenced by:  eqtr2i 1909  eqtr3i 1910  eqtr4i 1911  3eqtri 1912  3eqtrri 1913  3eqtr2i 1915  3eqtr3iOLD 1919  3eqtr4iOLD 1922  rababOLD 2309  cbvrab 2421  difjust 2595  unjust 2598  injust 2601  difeq12i 2724  dfun3 2833  dfin3 2834  invdif 2836  difundi 2847  difindi 2849  symdif1 2856  disjssun 2932  undif1 2949  inundifOLD 2952  dfif2 2984  ifbieq2i 2997  pwjust 3033  snjust 3047  dfpr2 3059  tprot 3103  dfuni2 3179  intab 3247  intunsn 3254  iunid 3308  viin 3314  iinrab 3318  iinrab2 3319  2iunin 3323  unopab 3410  dfepfrOLD 3641  orddif 3764  op1stb 3857  ordunisuc 3911  onuninsuci 3921  fconstopab 4031  onnev 4070  inxp 4109  dfdm3 4148  dfrn3 4150  dmun 4163  dmopab 4167  dmopab3 4169  dmxpin 4180  rnopab 4201  rncoss 4213  rncoeq 4217  resundi 4229  resindi 4231  resopab 4252  dfima3 4267  dfima3OLD 4268  imadisj 4285  ndmima 4300  rnun 4325  imaundi 4328  cnvxp 4332  rnxp 4342  dminxp 4357  dmprop 4369  op1sta 4372  opswap 4374  op2ndb 4376  op2nda 4377  op2ndaOLD 4378  rescnvcnvOLD 4386  resdmres 4390  dfco2aOLD 4395  coundi 4396  coundir 4398  cocnvcnv1 4408  cores2 4410  dfdm2 4421  funi 4452  funtp 4468  funcnvuni 4482  funcnvres 4487  fnresdisj 4523  resdif 4659  fv2 4676  fv2OLD 4677  dfimafn2 4721  fvopab4gf 4744  fvsnun1 4764  abrexexlem2 4835  opreq12iOLD 4895  resoprab 4938  oprabval 4952  oprabvalig 4953  oprabval2gf 4955  oprabval5 4958  caopr31 4995  caopr42 4999  caoprdilem 5001  caoprmo 5003  cbvmpt 5011  fvmptg 5014  ovmpt2g 5016  op1st 5026  op2nd 5027  f1stres 5034  f2ndres 5035  unielxp 5047  dfopab2 5053  dfoprab3 5054  dfoprab3s 5055  dfoprab5sf 5058  curry1 5075  curry2 5078  fpar 5085  iotajust 5088  dfiota2 5090  tfrlem3 5121  tfrlem9 5127  tfrlem10 5128  tz7.44-2 5137  dfrdg2 5141  rdglem1 5145  rdgsucopabn 5155  frsucmpt 5163  abianfplem 5170  df1o2 5185  ecidsn 5345  oprec 5377  fnmap 5388  mapvalg 5389  pmvalg 5390  map0 5403  xpassen 5500  ac6sfi 5509  sbthlem5 5514  sbthlem8 5517  fodomr 5547  mapunen 5596  ssenen 5598  limensuci 5600  phplem1 5602  abfii4 5654  abfii5 5655  pm54.43 5662  supex 5667  ordtypelem1 5684  ordtypelem6 5689  ordtype 5691  inf3lema 5715  inf3lemb 5716  trcl 5752  zfregs 5754  r10 5762  rankval 5779  rankuni 5809  ranksuc 5811  rankxpu 5822  rankxplim3 5825  rankxpsuc 5826  kardex 5855  hta 5858  aleph0 5874  aceq3 5895  ac6lem 5916  kmlem11 5937  kmlem12 5938  zorn2lem1 5950  brdom7disj 5966  brdom6disj 5967  alephfplem1 6044  cf0 6058  cdaval 6067  cdaassen 6080  addpiord 6164  mulpiord 6165  dmaddpi 6170  dmmulpi 6171  addcmpblnq 6204  addcompq 6214  dmrecpq 6226  ltapq 6228  ltmpq 6229  1lt2pq 6230  ltaddpq 6231  mulcomsr 6350  distrsr 6352  ltasr 6361  recexsrlem 6364  sqgt0sr 6367  map2psrpr 6372  supsrlem4 6380  supsrlem5 6381  addcnsr 6405  mulcnsr 6406  mulresr 6409  axmulcom 6429  axmulass 6431  axdistr 6432  axi2m1 6438  axcnre 6439  mulid2i 6486  add42i 6497  negsubiOLD 6539  neg0 6575  mul02i 6595  1p1timesi 6596  mul2negi 6610  negdii 6611  negdiiOLD 6612  mnfnre 6666  renfdisjOLD 6713  ssxr 6714  ssxrOLD 6715  ltsubaddiOLD 6770  divcan1i 6906  divreci 6920  divcan3i 6934  divcan4i 6935  dividi 6946  recgt0ii 6992  2timesi 7187  2t2e4 7206  3t2e6 7207  3t3e9 7208  4t2e8 7209  5t2e10 7210  8th4div3 7217  halfpm6th 7218  infmsup 7277  nneoi 7409  uzwo3lem2 7430  intfrac2 7495  intfracq 7496  dfioo2 7572  icoshftf1oii 7578  uzinfmi 7631  nninfm 7632  nn0infm 7633  fztpval 7688  om2uz0i 7706  uzrdginii 7715  seq1lem1 7722  seq1rval 7724  ser11i 7748  shftidt 7768  seq1seq01 7787  seq00 7793  ser00i 7809  sqrecii 7864  sumsqne0i 7879  sq2 7883  sq3 7884  cu2 7885  binom2i 7890  binom2aiOLD 7891  discrlem1 7906  nn0opthlem1 7914  sqrlem10 7932  sqrlem11 7933  sqrlem16 7938  sqrthi 7949  sqr2irrlem1 7974  i2 7982  i3 7983  crne0i 7989  imre 8023  cjcji 8028  recji 8032  imcji 8033  readdi 8034  imaddi 8035  remuli 8036  immuli 8037  cjaddi 8038  renegi 8044  imnegi 8046  cjnegi 8047  cji 8077  absval2i 8092  abs00i 8093  absmuli 8098  absidi 8112  abstrii 8143  fac0 8186  fac1 8187  facp1 8188  fac2 8189  faclbnd4lem1 8200  faclbnd4lem4 8203  bcpasc2i 8219  hashgval 8230  sumeq12i 8249  serzfsum 8264  csbfsumlem 8286  dfisum 8452  isumnn0nnai 8469  isum0spliti 8478  arisumilem 8486  geoseri 8496  geolim1i 8500  0.999... 8508  fsum0diag 8520  fsum0diag2 8521  ivthlem6 8548  ivthlem7 8549  dsupivthlem 8553  ef0lem 8572  efseq0ex 8573  efcvgfsum 8577  erelem2 8582  erelem6 8586  ele3lem 8588  ege2le3lem2 8591  efaddlem5 8604  efaddlem8 8607  efaddlem20 8619  efaddlem22 8621  ef1tllem 8643  eirrlem1 8651  eirrlem2 8652  efsepi 8661  ef4pi 8664  reeff1 8675  efm1limi 8676  sin0 8709  cos0 8711  sinaddi 8716  cosaddi 8717  cos1bnd 8740  cos2bnd 8741  acdc3lem 8754  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  ruclem2 8780  ruclem3 8781  ruclem14 8792  ruclem15 8793  infxpidmlem6 8826  infxpidmlem11 8831  infmap2lem1 8848  subbas2 8915  subtop 8916  indistop 8918  fctop 8920  cctop 8922  uniretop 8927  cnco 9045  dfms2 9076  metssba 9086  cnmetdval 9180  cnmetba 9181  cncfmet 9183  cncfmet1 9184  remetdval 9186  oprcn 9255  bcthlem9 9285  gid0 9338  grpsn 9340  grpidvallem 9341  grpidval 9342  issubg 9425  gapm 9462  ringsn 9490  vcm 9522  vcnegneg 9525  vafval 9554  smfval 9556  nmfval 9558  nvnncan 9615  nvm1 9624  nvpi 9626  nvmtri 9631  cnnvg 9640  cnnvs 9643  abscn 9682  ipval2lem1 9690  ipval2 9696  ipid 9702  ip0r 9709  nmblolbii 9799  blocnilem 9804  ip2i 9828  ipdirilem 9829  ipasslem10 9840  siilem1 9852  siii 9854  minvecex 9923  spwval2 9996  pilem1 10020  pilem3 10022  sinhalfpilem 10028  cospi 10031  eulerid 10032  sin2pi 10033  cos2pi 10034  sinperlem1 10035  sincosq4sgn 10056  sincos4thpi 10060  sincos6thpi 10061  sinkpi 10063  cosh111lem1 10068  effoi 10099  pilog 10122  grothprim 10141  avril1 10142  oprabvaligg 10154  oprabco 10159  oprab2co 10160  mptfn 10162  rnmpt 10163  dif1en 10172  basmetres 10185  symgval 10202  symgidi 10206  uptx 10226  txcn 10227  2txcn 10229  subsp 10244  subtopmetlem 10255  fbssint 10279  filmapf 10307  flimff 10317  ismgm 10367  idrval 10374  on1el3 10412  ring1cl 10415  uznzr 10416  zrdivrng 10418  hvsubassi 10554  hvnegdii 10561  hvsubeq0i 10562  hvsubcan2i 10563  normlem0 10608  normlem1 10609  normlem9 10617  normsqi 10632  norm-ii.i 10637  norm-iii.i 10639  normsubi 10641  normpari 10654  normpar2i 10656  polid2i 10657  bcsiALT 10679  hhssva 10762  hhsssm 10763  hhssnv 10767  hhshsslem1 10770  hhsssh2 10773  projlem3 10821  projlem4 10822  projlem7 10825  projlem18 10836  pjthlem1 10852  ococi 10880  dfchsup2 10931  dfchj2 10957  dfchj3 10958  chdmm2i 11034  chdmm3i 11035  chdmm4i 11036  chdmj2i 11038  chdmj3i 11039  chdmj4i 11040  chjoi 11044  h1de2i 11109  spanunsni 11135  pjoml3i 11162  pjoml4i 11163  cmbr2i 11172  cmbr3i 11176  qlax5i 11207  qlaxr2i 11209  osumcor2i 11225  pjadjii 11253  pjaddii 11255  pjmulii 11257  pjsubii 11258  pjssmii 11261  pjdifnormii 11263  pjcji 11264  pjpythi 11302  mayetes3i 11310  dfiop2 11316  hoid1i 11352  hoid1ri 11353  honegneg 11369  hosd1i 11385  hosubeq0i 11389  ho01i 11391  dfadj2 11449  cnvadj 11453  adj1o 11455  dmadjss 11456  hhlnoi 11463  hh0oi 11466  lnop0 11527  nmop0h 11553  lnopunilem1 11572  lnophmlem2 11579  nmbdoplbi 11586  lnfn0i 11608  cnlnadjlem5 11641  adjbdln 11653  nmoptri2i 11669  kbass2 11688  kbass5 11691  mdsl1i 11893  cvmdi 11896  mdsldmd1i 11903  mdslmd3i 11904  mdexchi 11907  shatomistici 11933  cvexchi 11941  atordi 11956  sumdmdlem2 11991  foo3 12015  bnj536 12532  bnj1271 13030  bnj1366 13091  bnj1504 13165  bnj1534 13183  bnj98 13221  bnj873 13317  bnj882 13320  bnj1390 13513  ifbieq2iOLD 13593  ghomgrpilem2 13629  ghomgrp 13633  cayleylem3 13643  divalglem5 13700  divalglem6 13701  gcd0val 13716  gcdcllem3 13720  gcdaddmlem 13734  algr0 13740  eucalgval 13749  eucalgcvga 13754  mulgcdlem2 13757  mulgcdlem5 13760  fresin 13840  mpt2fun 13843  dfon2 13858  domep 13861  dfpred2 13887  frsucopabn 13911  wfi 13915  frind 13939  poseq 13954  soseq 13955  wfrlem1 13957  wfrlem5 13961  wfrlem7 13963  wfrlem9 13965  wfrlem12 13968  wfrlem13 13969  wfrlem14 13970  tfr1ALT 13977  tfr2ALT 13978  tfr3ALT 13979  axfelem9 14039  axfelem15 14045  axfelem17 14047  dfon3 14072  dfom5 14081  dmoprabss6 14336  fldcnv 14359  cnvref 14371  fldsqcp2 14378  opreq123i 14410  fnoprab2ga 14470  fnoprab2a 14471  dmoprab2a 14472  foprab2a 14473  oprabval2ga 14474  oprabex2ga 14475  fvopab2b 14476  fopab2ga 14478  fopab2a 14479  rngop 14484  cbicp 14509  iscst1 14519  3timesi 14523  domrancur1b 14548  domrancur1c 14550  empos 14583  dominc 14622  rninc 14623  domncnt 14624  ranncnt 14625  dfps2 14634  valproemset 14657  prodeq123i 14664  expmiz 14724  gaplc 14731  cmprtr 14760  cmprtr2 14761  prsubrtr2 14764  zerdivemp1 14785  rngridfz 14786  vecax4 14799  vecax5 14800  invaddvec 14810  prodvs 14811  dblsubvec 14817  mvecrtol2 14820  mulinvsca 14823  muldisc 14824  vecax5c 14825  svli2 14826  svs2 14829  svs3 14830  dmhmph 14886  rnhmph 14887  top2usne 14898  sbtpsines 14905  limfillem1 14938  limfillem2 14939  singempcon 14965  idtrgrp 14978  invtrgrp 14979  topgrpsubcn 14982  trhom 14983  cntrsetlem 14999  cntrset 15000  domleqt 15020  fldleqt 15023  mpinf 15027  miminf 15028  flimfneic 15036  domval 15070  codval 15071  idval 15072  cmpval 15073  1ded 15085  1cat 15106  dmo 15123  cmpmorp 15126  ishomb 15137  mrdmcd 15143  homib 15145  cmphmia 15147  cmphmib 15148  iri 15149  idmon 15166  issubcat 15193  idsubidsup 15205  taralt 15211  tarval2 15249  fictblem 15370  fictb 15371  ordtypelem1OLD 15375  ordtypelem6OLD 15380  ordtypeOLD 15382  cldbnd 15410  alexsublem3 15439  locfincomp 15514  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  filcon 15580  ufcondr 15581  fclusff 15623  rabnc 15668  fnimapr 15687  oprabvalg 15706  oprabrexex2 15709  opropabco 15712  eroprlem 15732  fdc 15812  csbrni 15832  trirni 15833  iccst 15875  idcncf 15884  txcnoprab 15911  cnoprab1 15921  cnoprab2 15922  txmet 15925  ismtyres 15954  heiborlem11 15965  heiborlem18 15972  bfplem3 16000  bfplem6 16003  ismrer1 16024  iccbnd 16026  icccmp 16027  phtpycom 16050  phtpycolem2 16052  phtpycolem3 16053  phtpycolem4 16054  phtpyco 16056  reparphtlem2 16064  pcoval2 16075  pco1 16078  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  ringnegmn1l 16102  ringnegmn1r 16103  ringneglmul 16104  ringnegrmul 16105  zerdivemp1x 16108  isdivrng2 16111  rngkerinj 16129  iscring2 16146  1idl 16174  0ring 16175  smprngpr 16200  prnc 16215  isfldidl 16216  isdmn3 16222  cbvrabcsf 16414  compab 16418  smores2 16447  dfstruct2 16709  stbel 16729  stb2xpl 16742  stb3xpl 16743  glbconx 17029  padd02 17273  polval2 17319  pol0 17322

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain