Theorem eqtr4i 2763

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 2746	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2760	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtr2i  2766  3eqtr2ri  2767  3eqtr4i  2770  3eqtr4ri  2771  rabab  3473  cbvralcsf  3893  cbvrabcsf  3896  dfin5  3911  dfdif2  3912  uneqin  4243  notabw  4267  unrab  4269  inrab  4270  inrab2  4271  difrab  4272  dfrab3ss  4277  rabun2  4278  dfnul2  4290  difid  4330  rabxm  4344  elnelun  4347  abf  4360  difdifdir  4446  dfif3  4496  dfif5  4498  rabsnif  4682  tpidm  4717  ssunpr  4792  sstp  4794  opidg  4850  dfint2  4906  iunrab  5010  uniiun  5016  intiin  5017  iunid  5018  0iin  5021  mptv  5206  dfepfr  5616  epfrc  5617  xpundi  5701  xpundir  5702  csbcnv  5840  resiun2  5967  resopab  6001  mptresid  6018  dffr3  6066  dfse2  6067  cnvun  6108  imaundir  6116  imainrect  6147  cnvcnv2  6159  cnvrescnv  6161  cnvcnvres  6171  dmtpop  6184  rnsnopg  6187  resdifdi  6202  rnco2  6220  dmco  6221  co01  6228  unidmrn  6245  dfdm2  6247  predidm  6292  dfmpt3  6634  mptun  6646  funcocnv2  6807  dffv2  6937  fnasrn  7100  fpr  7109  fmptap  7126  rnmptc  7163  riotav  7330  dmoprab  7471  rnoprab2  7474  mpov  7480  mpomptx  7481  abrexex2g  7918  1stval2  7960  2ndval2  7961  fo1st  7963  fo2nd  7964  xp2  7980  dfoprab4f  8010  offval22  8040  fmpoco  8047  fimaproj  8087  tposmpo  8215  tposconst  8216  recsfval  8322  rdgsucmpt2  8371  frsucmpt2  8381  df2o3  8415  o1p1e2  8477  o2p2e4  8478  oarec  8499  omopthlem2  8598  dfqs2  8652  ecqs  8728  qliftf  8754  erovlem  8762  fset0  8803  mapsnf1o3  8845  ixp0x  8876  omf1o  9020  xpf1o  9079  mapunen  9086  enp1ilem  9190  marypha1lem  9348  marypha2lem4  9353  dfoi  9428  infeq5i  9557  oemapso  9603  cantnflem1  9610  rankelop  9798  leweon  9933  r0weon  9934  kmlem11  10083  dju1dif  10095  ackbij1lem16  10156  cf0  10173  cfsmolem  10192  alephsuc3  10503  fpwwe  10569  canthp1lem1  10575  wuncval2  10670  prlem936  10970  m1p1sr  11015  m1m1sr  11016  dfcnqs  11065  ssxr  11214  mul02lem2  11322  addrid  11325  2p2e4  12287  3p2e5  12303  3p3e6  12304  4p2e6  12305  4p3e7  12306  4p4e8  12307  5p2e7  12308  5p3e8  12309  5p4e9  12310  6p2e8  12311  6p3e9  12312  7p2e9  12313  nnzrab  12531  nn0zrab  12532  dec0u  12640  dec0h  12641  decsuc  12650  decsucc  12660  numma  12663  decma  12670  decmac  12671  decma2c  12672  decadd  12673  decaddc  12674  decmul1c  12684  decmul2c  12685  5p5e10  12690  6p4e10  12691  7p3e10  12694  8p2e10  12699  5t5e25  12722  6t6e36  12727  8t6e48  12738  nn0uz  12801  nnuz  12802  xaddcom  13167  x2times  13226  ioomax  13350  iccmax  13351  ioopos  13352  ioorp  13353  prunioo  13409  fseq1p1m1  13526  fzo13pr  13677  fzo0to2pr  13678  fzo0to3tp  13680  om2uzrdg  13891  fzennn  13903  irec  14136  sq10e99m1  14200  facnn  14210  fac0  14211  faclbnd2  14226  faclbnd4lem1  14228  hashfun  14372  hashbclem  14387  hashf1lem1  14390  hashf1lem2  14391  fz1isolem  14396  swrdccatin1  14660  swrdccat3blem  14674  s1co  14768  s2eq2s1eq  14871  s3eqs2s1eq  14873  ofs2  14906  dfid5  14962  dfid6  14963  fsumrev2  15717  fsumparts  15741  fsumiun  15756  isumnn0nn  15777  harmonic  15794  fprod2d  15916  bpoly2  15992  bpoly3  15993  bpoly4  15994  ege2le3  16025  cos1bnd  16124  efieq1re  16136  eirrlem  16141  qnnen  16150  cpnnen  16166  ruclem6  16172  3dvds  16270  pwp1fsum  16330  m1bits  16379  nn0expgcd  16503  algrp1  16513  phiprmpw  16715  prmreclem4  16859  4sqlem11  16895  4sqlem19  16903  dec5dvds  17004  decsplit1  17021  5prm  17048  7prm  17050  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  strle1  17097  grpbasex  17224  grpplusgx  17225  quslem  17476  xpsrnbas  17504  acsfn1  17596  acsfn2  17598  comfffval2  17636  dfinito2  17939  dftermo2  17940  xpchomfval  18114  xpccofval  18117  1stfval  18126  2ndfval  18129  oduleg  18225  chnub  18557  ismgmid  18602  efmndbas  18808  smndex2dnrinv  18852  grpinvfvi  18924  gaorb  19248  elcntr  19271  cntri  19273  cntrsubgnsg  19284  cntrnsg  19285  setsplusg  19291  oppgcntr  19306  gsumwrev  19307  symgressbas  19323  symgplusg  19324  symgvalstruct  19338  symgga  19348  cayleylem1  19353  psgnunilem2  19436  efgval2  19665  efgredlemc  19686  efgcpbllema  19695  frgpnabllem1  19814  gsumzaddlem  19862  gsumle  20086  opprlem  20290  oppr0  20297  opprneg  20299  rmodislmod  20893  rlmscaf  21171  xrsds  21376  gsumfsum  21401  zringunit  21433  pzriprng1  21465  cnmsgngrp  21546  psgnfix2  21566  relt  21582  ocv0  21644  thlle  21664  thlleval  21665  dsmmval2  21703  frlmip  21745  mplbas  21957  mplplusg  21974  mplmulr  21975  mplvsca2  21981  ressmplbas2  21994  ltbwe  22011  evlslem4  22043  psdmul  22121  psr1bas2  22142  ply1bas  22147  ply1basOLD  22148  ply1assa  22152  psr1plusg  22173  psr1vsca  22174  psr1mulr  22175  ply1plusg  22176  ply1vsca  22177  ply1mulr  22178  ply1mpl0  22209  ply1mpl1  22211  coe1mul  22224  matgsum  22393  smadiadetglem1  22627  indistpsx  22966  iuncld  23001  tgrest  23115  resstopn  23142  leordtval2  23168  xkouni  23555  ptclsg  23571  ptuncnv  23763  ptunhmeo  23764  alexsubALTlem4  24006  tsmsf1o  24101  ucnimalem  24235  ressxms  24481  uniretop  24718  cnfldtopn  24737  xrtgioo  24763  zcld  24770  icccmp  24782  xrge0gsumle  24790  xrge0tsms  24791  metnrmlem3  24818  fsum2cn  24830  cnmpopc  24890  oprpiece1res1  24917  oprpiece1res2  24918  evth  24926  evth2  24927  om1opn  25004  pi1xfrf  25021  pi1xfrcnv  25025  pi1cof  25027  clsocv  25218  cncmet  25290  cnflduss  25324  rrxprds  25357  ehlbase  25383  ismbl  25495  shftmbl  25507  ioorinv  25545  itg1addlem4  25668  itg2cnlem1  25730  itg0  25749  itgss3  25784  ditgneg  25826  limcdif  25845  limciun  25863  dvexp  25925  dvef  25952  dvcnvrelem2  25991  ftc1  26017  aannenlem2  26305  dvradcnv  26398  pserdvlem2  26406  reefgim  26428  cospi  26449  sincos6thpi  26493  tanregt0  26516  dflog2  26537  logfac  26578  dvlog  26628  cxpexp  26645  cxpmul2  26666  cxpsqrt  26680  dvsqrt  26719  dvcnsqrt  26721  cxpcn2  26724  isosctrlem2  26797  1cubrlem  26819  1cubr  26820  quart1lem  26833  atancj  26888  atanlogaddlem  26891  atansopn  26910  leibpilem2  26919  log2cnv  26922  log2ublem3  26926  birthdaylem1  26929  birthdaylem2  26930  birthday  26932  dfarea  26938  lgamgulmlem5  27011  lgambdd  27015  ftalem3  27053  basellem2  27060  ppiprm  27129  ppinprm  27130  chtprm  27131  chtnprm  27132  ppi2  27148  ppi3  27149  ppiub  27183  chtub  27191  bclbnd  27259  bposlem8  27270  lgsdilem  27303  lgsdir2lem2  27305  lgsquadlem2  27360  lgsquad2lem2  27364  2lgsoddprmlem3c  27391  rplogsum  27506  mulog2sumlem2  27514  pnt2  27592  bdayfo  27657  bday0  27819  bday1  27822  old1  27873  addsasslem2  28012  negbdaylem  28064  muls01  28120  abssnid  28251  1p1e2s  28424  n0seo  28429  twocut  28431  halfcut  28466  pw2cutp1  28469  pw2cut2  28470  istrkg2ld  28544  axsegconlem9  29010  ax5seglem7  29020  iedgedg  29135  uspgrf1oedg  29258  nbgrcl  29420  nbgrnvtx0  29424  rusgrprc  29676  pthsfval  29804  wlkiswwlks2lem4  29957  wlkiswwlks2lem5  29958  clwwlkvbij  30200  konigsbergumgr  30338  ex-pw  30516  ex-xp  30523  ex-rn  30527  nvvop  30697  nvm  30729  cnims  30781  ip0i  30913  ip1ilem  30914  ipdirilem  30917  ipasslem10  30927  h2hva  31062  h2hsm  31063  h2hvs  31065  axhfvadd-zf  31070  axhvcom-zf  31071  axhvass-zf  31072  axhv0cl-zf  31073  axhvaddid-zf  31074  axhfvmul-zf  31075  axhvmulid-zf  31076  axhvmulass-zf  31077  axhvdistr1-zf  31078  axhvdistr2-zf  31079  axhvmul0-zf  31080  axhfi-zf  31081  axhis1-zf  31082  axhis2-zf  31083  axhis3-zf  31084  axhis4-zf  31085  axhcompl-zf  31086  normlem0  31197  normlem1  31198  normlem2  31199  normlem4  31201  normlem9  31206  bcseqi  31208  dfhnorm2  31210  norm3difi  31235  normpari  31242  normpar2i  31244  polid2i  31245  polidi  31246  hhba  31255  hhims  31260  hhims2  31261  hhsssh  31357  hhssims  31362  hhssims2  31363  shsval3i  31476  dfch2  31495  cmcm2i  31681  fh2  31707  qlaxr3i  31724  spansnji  31734  pjcji  31772  ho0val  31838  df0op2  31840  hosd1i  31910  hosd2i  31911  eigorthi  31925  hhlnoi  31988  hhnmoi  31989  hhbloi  31990  bra0  32038  nmop0  32074  nmfn0  32075  lnopeq0lem1  32093  lnopunilem1  32098  lnophmlem2  32105  nmopcoadji  32189  pjhmopidm  32271  cvmdi  32412  cdj3lem3  32526  cdj3lem3b  32528  abrexdomjm  32594  uniin1  32638  uniin2  32639  iundifdifd  32648  iundifdif  32649  mpomptxf  32768  df1stres  32794  df2ndres  32795  intimafv  32801  fcobijfs  32811  fcobijfs2  32812  resf1o  32820  fpwrelmapffslem  32822  sgnneg  32925  dpval3  32986  dp3mul10  32990  dpadd2  33002  dpmul4  33006  ccatws1f1o  33044  xrslt  33100  xrsclat  33104  xrge0tsmsd  33167  cycpmco2lem7  33226  cycpmconjv  33236  cycpmrn  33237  conjga  33264  elrgspnsubrunlem2  33342  rndrhmcl  33390  fracf1  33401  xrge0slmod  33441  lsmsnorb2  33485  qusbas2  33499  1arithidomlem2  33629  zringfrac  33647  mplvrpmga  33722  mplvrpmmhm  33723  mplvrpmrhm  33724  psrmonprod  33729  mplmonprod  33731  vieta  33757  rlmdim  33787  rgmoddimOLD  33788  isconstr  33914  iconstr  33944  cos9thpiminplylem4  33963  cos9thpiminplylem5  33964  circtopn  34015  tpr2rico  34090  xrge0mulc1cn  34119  lmxrge0  34130  esumpfinvallem  34252  esumcocn  34258  hasheuni  34263  esumcvg  34264  rossros  34358  measinblem  34398  aean  34422  sxbrsigalem3  34450  dya2iocival  34451  dya2iocucvr  34462  sxbrsigalem1  34463  sxbrsigalem2  34464  sxbrsigalem5  34466  sxbrsiga  34468  fiunelcarsg  34494  eulerpartlem1  34545  eulerpartgbij  34550  fibp1  34579  coinfliplem  34657  coinflipprob  34658  ballotlemfval  34668  ballotth  34716  plymulx  34726  circlemethhgt  34821  hgt750lem2  34830  bnj1400  35011  bnj66  35036  bnj882  35102  lfuhgr  35334  derang0  35385  subfacp1lem1  35395  subfacp1lem6  35401  kur14lem7  35428  cvmsss2  35490  cvmliftlem8  35508  cvmliftlem10  35510  satfv1lem  35578  msubfval  35740  quad3  35886  bcprod  35954  bccolsum  35955  faclim  35962  pprodcnveq  36097  dfon4  36107  fobigcup  36114  dfiota3  36137  dfrecs2  36166  dfrdg4  36167  dfint3  36168  rankeq1o  36387  refssfne  36574  ssoninhaus  36664  onint1  36665  bj-dfnul2  36795  bj-rababw  37129  bj-inrab3  37177  bj-imdiridlem  37440  dissneq  37596  dffinxpf  37640  finxpreclem4  37649  rabiun  37844  ptrest  37870  poimirlem3  37874  poimirlem4  37875  poimirlem13  37884  poimirlem16  37887  poimirlem22  37893  poimirlem26  37897  poimirlem27  37898  poimirlem30  37901  cnambfre  37919  ftc1anclem8  37951  fnopabco  37974  abrexdom  37981  cncfres  38016  scottexf  38419  scott0f  38420  inres2  38498  eqrabi  38507  xpv  38513  dfres4  38550  dmxrn  38638  xrnres  38676  xrnres2  38677  rnqmap  38705  dfsucmap2  38715  dfcoss2  38754  dfcoss4  38756  1cossres  38770  dmcoss2  38795  1cosscnvxrn  38816  dfeqvrels2  38923  dfcoeleqvrels  38956  redundss3  38963  dffunsALTV5  39023  dfpeters2  39225  cdleme3d  40607  cdleme7a  40619  cdleme31sdnN  40763  cdlemk45  41323  420gcd8e4  42376  lcmeprodgcdi  42377  60lcm7e420  42380  420lcm8e840  42381  3lexlogpow5ineq1  42424  3lexlogpow2ineq1  42428  3lexlogpow2ineq2  42429  3lexlogpow5ineq5  42430  aks4d1p1  42446  posbezout  42470  aks6d1c1p4  42481  aks6d1c3  42493  2ap1caineq  42515  sticksstones7  42522  sticksstones12a  42527  sticksstones12  42528  aks6d1c6lem4  42543  imaopab  42603  fmpocos  42606  dfqs3  42609  decaddcom  42654  sumcubes  42683  redvmptabs  42730  readvrec  42732  readvcot  42734  sn-00idlem2  42769  reixi  42793  sum9cubes  43030  mapfzcons  43073  eldioph4b  43168  diophren  43170  pwssplit4  43446  pwfi2f1o  43453  frlmpwfi  43455  mendplusgfval  43538  mendmulrfval  43540  mendvscafval  43543  idomodle  43548  cytpval  43559  arearect  43572  onov0suclim  43631  omabs2  43689  tr3dom  43884  har2o  43902  alephiso2  43914  alephiso3  43915  relintab  43939  dfid7  43968  cnvrcl0  43981  dfrtrcl5  43985  dfrcl3  44031  dfrcl4  44032  comptiunov2i  44062  corcltrcl  44095  neicvgnvo  44471  inductionexd  44511  mnuprdlem2  44629  nznngen  44672  hashnzfz2  44677  lhe4.4ex1a  44685  dvradcnv2  44703  binomcxplemrat  44706  binomcxplemnotnn0  44712  nregmodelf1o  45371  refsum2cnlem1  45397  fiiuncl  45425  iccdifprioo  45876  lptre2pt  45998  limclner  46009  stoweidlem13  46371  stoweidlem32  46390  stoweidlem62  46420  wallispi2lem2  46430  stirlinglem14  46445  dirkertrigeqlem1  46456  dirkercncflem4  46464  fourierdlem42  46507  fourierdlem73  46537  fourierdlem81  46545  fourierdlem92  46556  fourierdlem103  46567  fourierdlem104  46568  fouriercnp  46584  fouriersw  46589  sge0tsms  46738  sge0iunmptlemfi  46771  ovolval5lem3  47012  cnfsmf  47098  nthrucw  47244  lamberte  47248  rnfdmpr  47641  fvmptrabdm  47653  fundcmpsurinjlem1  47758  m11nprm  47961  opoeALTV  48043  nfermltl8rev  48102  sbgoldbo  48147  evengpop3  48158  clnbgrcl  48181  clnbgrnvtx0  48187  usgrexmpl2edg  48389  usgrexmpl2nb0  48391  usgrexmpl2nb3  48394  gpg5order  48420  gpgprismgr4cycllem6  48460  cznabel  48620  cznrng  48621  mpomptx2  48695  2sphere  49109  itscnhlinecirc02plem3  49144  inlinecirc02p  49147  dftpos5  49233  tposresg  49237  icccldii  49278  dfnrm2  49291  dfnrm3  49292  elxpcbasex1ALT  49608  elxpcbasex2ALT  49610  dfswapf2  49620  swapf1a  49628  swapf1f1o  49634  swapf2f1oa  49636  swapfida  49639  setc1oterm  49850  setc1ohomfval  49852  setc1ocofval  49853  funcsetc1o  49856  dfinito4  49860  setc1onsubc  49961  islmd  50024  iscmd  50025  initocmd  50028  termolmd  50029  amgmlemALT  50162