Theorem eqtr4i 2765

Description: An equality transitivity inference. (Contributed by NM, 26-May-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	⊢ 𝐴 = 𝐵
eqtr4i.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eqtr4i	⊢ 𝐴 = 𝐶

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtr4i.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2743	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2762	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  3eqtr2i  2768  3eqtr2ri  2769  3eqtr4i  2772  3eqtr4ri  2773  rabab  3509  cbvralcsf  3952  cbvrabcsf  3955  dfin5  3970  dfdif2  3971  uneqin  4294  notabw  4318  unrab  4320  inrab  4321  inrab2  4322  difrab  4323  dfrab3ss  4328  rabun2  4329  dfnul2  4341  difid  4381  rabxm  4395  elnelun  4398  abf  4411  difdifdir  4497  dfif3  4544  dfif5  4546  rabsnif  4727  tpidm  4762  ssunpr  4838  sstp  4840  opidg  4896  dfint2  4952  iunrab  5056  uniiun  5062  intiin  5063  iunid  5064  0iin  5068  mptv  5263  dfepfr  5672  epfrc  5673  xpundi  5756  xpundir  5757  csbcnv  5896  resiun2  6020  resopab  6053  mptresid  6070  dffr3  6119  dfse2  6120  cnvun  6164  imaundir  6172  imainrect  6202  cnvcnv2  6214  cnvrescnv  6216  cnvcnvres  6226  dmtpop  6239  rnsnopg  6242  resdifdi  6257  rnco2  6274  dmco  6275  co01  6282  unidmrn  6300  dfdm2  6302  predidm  6348  tz6.26OLD  6370  dfmpt3  6702  mptun  6714  funcocnv2  6873  dffv2  7003  fnasrn  7164  fpr  7173  fmptap  7189  rnmptc  7226  riotav  7392  dmoprab  7534  rnoprab2  7537  mpov  7544  mpomptx  7545  abrexex2g  7987  1stval2  8029  2ndval2  8030  fo1st  8032  fo2nd  8033  xp2  8049  dfoprab4f  8079  offval22  8111  fmpoco  8118  fimaproj  8158  tposmpo  8286  tposconst  8287  recsfval  8419  rdgsucmpt2  8468  frsucmpt2  8478  df2o3  8512  o1p1e2  8576  o2p2e4  8577  oarec  8598  omopthlem2  8696  ecqs  8819  qliftf  8843  erovlem  8851  fset0  8892  mapsnf1o3  8933  ixp0x  8964  omf1o  9113  xpf1o  9177  mapunen  9184  enp1ilem  9309  marypha1lem  9470  marypha2lem4  9475  dfoi  9548  infeq5i  9673  oemapso  9719  cantnflem1  9726  rankelop  9911  leweon  10048  r0weon  10049  kmlem11  10198  dju1dif  10210  ackbij1lem16  10271  cf0  10288  cfsmolem  10307  alephsuc3  10617  fpwwe  10683  canthp1lem1  10689  wuncval2  10784  prlem936  11084  m1p1sr  11129  m1m1sr  11130  dfcnqs  11179  ssxr  11327  mul02lem2  11435  addrid  11438  2p2e4  12398  3p2e5  12414  3p3e6  12415  4p2e6  12416  4p3e7  12417  4p4e8  12418  5p2e7  12419  5p3e8  12420  5p4e9  12421  6p2e8  12422  6p3e9  12423  7p2e9  12424  nnzrab  12642  nn0zrab  12643  dec0u  12751  dec0h  12752  decsuc  12761  decsucc  12771  numma  12774  decma  12781  decmac  12782  decma2c  12783  decadd  12784  decaddc  12785  decmul1c  12795  decmul2c  12796  5p5e10  12801  6p4e10  12802  7p3e10  12805  8p2e10  12810  5t5e25  12833  6t6e36  12838  8t6e48  12849  nn0uz  12917  nnuz  12918  xaddcom  13278  x2times  13337  ioomax  13458  iccmax  13459  ioopos  13460  ioorp  13461  prunioo  13517  fseq1p1m1  13634  fzo13pr  13784  fzo0to2pr  13785  fzo0to3tp  13787  om2uzrdg  13993  fzennn  14005  irec  14236  sq10e99m1  14300  facnn  14310  fac0  14311  faclbnd2  14326  faclbnd4lem1  14328  hashfun  14472  hashbclem  14487  hashf1lem1  14490  hashf1lem2  14491  fz1isolem  14496  swrdccatin1  14759  swrdccat3blem  14773  s1co  14868  s2eq2s1eq  14971  s3eqs2s1eq  14973  ofs2  15006  dfid5  15062  dfid6  15063  fsumrev2  15814  fsumparts  15838  fsumiun  15853  isumnn0nn  15874  harmonic  15891  fprod2d  16013  bpoly2  16089  bpoly3  16090  bpoly4  16091  ege2le3  16122  cos1bnd  16219  efieq1re  16231  eirrlem  16236  qnnen  16245  cpnnen  16261  ruclem6  16267  3dvds  16364  pwp1fsum  16424  m1bits  16473  nn0expgcd  16597  algrp1  16607  phiprmpw  16809  prmreclem4  16952  4sqlem11  16988  4sqlem19  16996  dec5dvds  17097  decsplit1  17115  5prm  17142  7prm  17144  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  strle1  17191  grpbasex  17336  grpplusgx  17337  quslem  17589  xpsrnbas  17617  acsfn1  17705  acsfn2  17707  comfffval2  17745  dfinito2  18056  dftermo2  18057  xpchomfval  18234  xpccofval  18237  1stfval  18246  2ndfval  18249  oduleg  18346  ismgmid  18690  efmndbas  18896  smndex2dnrinv  18940  grpinvfvi  19012  gaorb  19337  elcntr  19360  cntri  19362  cntrsubgnsg  19373  cntrnsg  19374  setsplusg  19380  oppglemOLD  19381  oppgcntr  19398  gsumwrev  19399  symgressbas  19413  symgplusg  19414  symgvalstruct  19428  symgvalstructOLD  19429  symgga  19439  cayleylem1  19444  psgnunilem2  19527  efgval2  19756  efgredlemc  19777  efgcpbllema  19786  frgpnabllem1  19905  gsumzaddlem  19953  mgplemOLD  20156  opprlem  20355  opprlemOLD  20356  oppr0  20365  opprneg  20367  rmodislmod  20944  rmodislmodOLD  20945  rlmscaf  21231  xrsds  21444  gsumfsum  21469  zringunit  21494  pzriprng1  21526  cnmsgngrp  21614  psgnfix2  21634  relt  21650  ocv0  21712  thlle  21733  thlleOLD  21734  thlleval  21735  dsmmval2  21773  frlmip  21815  mplbas  22027  mplplusg  22044  mplmulr  22045  mplvsca2  22051  ressmplbas2  22062  ltbwe  22079  evlslem4  22117  psdmul  22187  psr1bas2  22206  ply1bas  22211  ply1basOLD  22212  ply1assa  22216  psr1plusg  22237  psr1vsca  22238  psr1mulr  22239  ply1plusg  22240  ply1vsca  22241  ply1mulr  22242  ply1mpl0  22273  ply1mpl1  22275  coe1mul  22288  matgsum  22458  smadiadetglem1  22692  indistpsx  23032  iuncld  23068  tgrest  23182  resstopn  23209  leordtval2  23235  xkouni  23622  ptclsg  23638  ptuncnv  23830  ptunhmeo  23831  alexsubALTlem4  24073  tsmsf1o  24168  ucnimalem  24304  ressxms  24553  uniretop  24798  cnfldtopn  24817  xrtgioo  24841  zcld  24848  icccmp  24860  xrge0gsumle  24868  xrge0tsms  24869  metnrmlem3  24896  fsum2cn  24908  cnmpopc  24968  oprpiece1res1  24995  oprpiece1res2  24996  evth  25004  evth2  25005  om1opn  25082  pi1xfrf  25099  pi1xfrcnv  25103  pi1cof  25105  clsocv  25297  cncmet  25369  cnflduss  25403  rrxprds  25436  ehlbase  25462  ismbl  25574  shftmbl  25586  ioorinv  25624  itg1addlem4  25747  itg1addlem4OLD  25748  itg2cnlem1  25810  itg0  25829  itgss3  25864  ditgneg  25906  limcdif  25925  limciun  25943  dvexp  26005  dvef  26032  dvcnvrelem2  26071  ftc1  26097  aannenlem2  26385  dvradcnv  26478  pserdvlem2  26486  reefgim  26508  cospi  26528  sincos6thpi  26572  tanregt0  26595  dflog2  26616  logfac  26657  dvlog  26707  cxpexp  26724  cxpmul2  26745  cxpsqrt  26759  dvsqrt  26798  dvcnsqrt  26800  cxpcn2  26803  isosctrlem2  26876  1cubrlem  26898  1cubr  26899  quart1lem  26912  atancj  26967  atanlogaddlem  26970  atansopn  26989  leibpilem2  26998  log2cnv  27001  log2ublem3  27005  birthdaylem1  27008  birthdaylem2  27009  birthday  27011  dfarea  27017  lgamgulmlem5  27090  lgambdd  27094  ftalem3  27132  basellem2  27139  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  ppi2  27227  ppi3  27228  ppiub  27262  chtub  27270  bclbnd  27338  bposlem8  27349  lgsdilem  27382  lgsdir2lem2  27384  lgsquadlem2  27439  lgsquad2lem2  27443  2lgsoddprmlem3c  27470  rplogsum  27585  mulog2sumlem2  27593  pnt2  27671  bdayfo  27736  bday0s  27887  bday1s  27890  old1  27928  addsasslem2  28051  negsbdaylem  28102  muls01  28152  abssnid  28281  1p1e2s  28414  n0seo  28419  nohalf  28421  zs12bday  28438  istrkg2ld  28482  axsegconlem9  28954  ax5seglem7  28964  iedgedg  29081  uspgrf1oedg  29204  nbgrcl  29366  nbgrnvtx0  29370  rusgrprc  29622  pthsfval  29753  wlkiswwlks2lem4  29901  wlkiswwlks2lem5  29902  clwwlkvbij  30141  konigsbergumgr  30279  ex-pw  30457  ex-xp  30464  ex-rn  30468  nvvop  30637  nvm  30669  cnims  30721  ip0i  30853  ip1ilem  30854  ipdirilem  30857  ipasslem10  30867  h2hva  31002  h2hsm  31003  h2hvs  31005  axhfvadd-zf  31010  axhvcom-zf  31011  axhvass-zf  31012  axhv0cl-zf  31013  axhvaddid-zf  31014  axhfvmul-zf  31015  axhvmulid-zf  31016  axhvmulass-zf  31017  axhvdistr1-zf  31018  axhvdistr2-zf  31019  axhvmul0-zf  31020  axhfi-zf  31021  axhis1-zf  31022  axhis2-zf  31023  axhis3-zf  31024  axhis4-zf  31025  axhcompl-zf  31026  normlem0  31137  normlem1  31138  normlem2  31139  normlem4  31141  normlem9  31146  bcseqi  31148  dfhnorm2  31150  norm3difi  31175  normpari  31182  normpar2i  31184  polid2i  31185  polidi  31186  hhba  31195  hhims  31200  hhims2  31201  hhsssh  31297  hhssims  31302  hhssims2  31303  shsval3i  31416  dfch2  31435  cmcm2i  31621  fh2  31647  qlaxr3i  31664  spansnji  31674  pjcji  31712  ho0val  31778  df0op2  31780  hosd1i  31850  hosd2i  31851  eigorthi  31865  hhlnoi  31928  hhnmoi  31929  hhbloi  31930  bra0  31978  nmop0  32014  nmfn0  32015  lnopeq0lem1  32033  lnopunilem1  32038  lnophmlem2  32045  nmopcoadji  32129  pjhmopidm  32211  cvmdi  32352  cdj3lem3  32466  cdj3lem3b  32468  abrexdomjm  32534  uniin1  32571  uniin2  32572  iundifdifd  32581  iundifdif  32582  mpomptxf  32693  df1stres  32718  df2ndres  32719  intimafv  32725  fcobijfs  32740  resf1o  32747  fpwrelmapffslem  32749  dpval3  32860  dp3mul10  32864  dpadd2  32876  dpmul4  32880  ccatws1f1o  32920  chnub  32985  xrslt  32991  xrsclat  32995  xrge0tsmsd  33047  gsumle  33083  cycpmco2lem7  33134  cycpmconjv  33144  cycpmrn  33145  rndrhmcl  33279  fracf1  33288  xrge0slmod  33355  lsmsnorb2  33399  qusbas2  33413  1arithidomlem2  33543  zringfrac  33561  rlmdim  33636  rgmoddimOLD  33637  circtopn  33797  tpr2rico  33872  xrge0mulc1cn  33901  lmxrge0  33912  esumpfinvallem  34054  esumcocn  34060  hasheuni  34065  esumcvg  34066  rossros  34160  measinblem  34200  aean  34224  sxbrsigalem3  34253  dya2iocival  34254  dya2iocucvr  34265  sxbrsigalem1  34266  sxbrsigalem2  34267  sxbrsigalem5  34269  sxbrsiga  34271  fiunelcarsg  34297  eulerpartlem1  34348  eulerpartgbij  34353  fibp1  34382  coinfliplem  34459  coinflipprob  34460  ballotlemfval  34470  ballotth  34518  sgnneg  34521  plymulx  34541  circlemethhgt  34636  hgt750lem2  34645  bnj1400  34827  bnj66  34852  bnj882  34918  lfuhgr  35101  derang0  35153  subfacp1lem1  35163  subfacp1lem6  35169  kur14lem7  35196  cvmsss2  35258  cvmliftlem8  35276  cvmliftlem10  35278  satfv1lem  35346  msubfval  35508  quad3  35654  bcprod  35717  bccolsum  35718  faclim  35725  pprodcnveq  35864  dfon4  35874  fobigcup  35881  dfiota3  35904  dfrecs2  35931  dfrdg4  35932  dfint3  35933  rankeq1o  36152  refssfne  36340  ssoninhaus  36430  onint1  36431  bj-rababw  36863  bj-inrab3  36911  bj-imdiridlem  37167  dissneq  37323  dffinxpf  37367  finxpreclem4  37376  rabiun  37579  ptrest  37605  poimirlem3  37609  poimirlem4  37610  poimirlem13  37619  poimirlem16  37622  poimirlem22  37628  poimirlem26  37632  poimirlem27  37633  poimirlem30  37636  cnambfre  37654  ftc1anclem8  37686  fnopabco  37709  abrexdom  37716  cncfres  37751  scottexf  38154  scott0f  38155  inres2  38226  dfres4  38274  xrnres  38383  xrnres2  38384  dfcoss2  38394  dfcoss4  38396  1cossres  38410  dmcoss2  38435  1cosscnvxrn  38456  dfeqvrels2  38569  dfcoeleqvrels  38602  redundss3  38609  dffunsALTV5  38668  cdleme3d  40213  cdleme7a  40225  cdleme31sdnN  40369  cdlemk45  40929  420gcd8e4  41987  lcmeprodgcdi  41988  60lcm7e420  41991  420lcm8e840  41992  3lexlogpow5ineq1  42035  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1  42057  posbezout  42081  aks6d1c1p4  42092  aks6d1c3  42104  2ap1caineq  42126  sticksstones7  42133  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem4  42154  imaopab  42248  fmpocos  42253  dfqs2  42256  dfqs3  42257  decaddcom  42297  sumcubes  42325  redvmptabs  42368  readvrec  42370  sn-00idlem2  42405  reixi  42428  sum9cubes  42658  mapfzcons  42703  eldioph4b  42798  diophren  42800  pwssplit4  43077  pwfi2f1o  43084  frlmpwfi  43086  mendplusgfval  43169  mendmulrfval  43171  mendvscafval  43174  idomodle  43179  cytpval  43190  arearect  43203  onov0suclim  43263  omabs2  43321  tr3dom  43517  har2o  43535  alephiso2  43547  alephiso3  43548  relintab  43572  dfid7  43601  cnvrcl0  43614  dfrtrcl5  43618  dfrcl3  43664  dfrcl4  43665  comptiunov2i  43695  corcltrcl  43728  neicvgnvo  44104  inductionexd  44144  mnuprdlem2  44268  nznngen  44311  hashnzfz2  44316  lhe4.4ex1a  44324  dvradcnv2  44342  binomcxplemrat  44345  binomcxplemnotnn0  44351  refsum2cnlem1  44974  fiiuncl  45004  iccdifprioo  45468  lptre2pt  45595  limclner  45606  stoweidlem13  45968  stoweidlem32  45987  stoweidlem62  46017  wallispi2lem2  46027  stirlinglem14  46042  dirkertrigeqlem1  46053  dirkercncflem4  46061  fourierdlem42  46104  fourierdlem73  46134  fourierdlem81  46142  fourierdlem92  46153  fourierdlem103  46164  fourierdlem104  46165  fouriercnp  46181  fouriersw  46186  sge0tsms  46335  sge0iunmptlemfi  46368  ovolval5lem3  46609  cnfsmf  46695  rnfdmpr  47230  fvmptrabdm  47242  fundcmpsurinjlem1  47322  m11nprm  47525  opoeALTV  47607  nfermltl8rev  47666  sbgoldbo  47711  evengpop3  47722  clnbgrcl  47745  clnbgrnvtx0  47751  usgrexmpl2edg  47923  usgrexmpl2nb0  47925  usgrexmpl2nb3  47928  gpg5order  47948  cznabel  48103  cznrng  48104  mpomptx2  48179  2sphere  48598  itscnhlinecirc02plem3  48633  inlinecirc02p  48636  icccldii  48714  dfnrm2  48727  dfnrm3  48728  amgmlemALT  49033