Theorem eqtr4i 2764

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 2742	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2761	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  3eqtr2i  2767  3eqtr2ri  2768  3eqtr4i  2771  3eqtr4ri  2772  rabab  3503  cbvralcsf  3939  cbvrabcsf  3942  dfin5  3957  dfdif2  3958  uneqin  4279  notabw  4304  unrab  4306  inrab  4307  inrab2  4308  difrab  4309  dfrab3ss  4313  rabun2  4314  dfnul2  4326  difid  4371  rabxm  4387  elnelun  4390  abf  4403  difdifdir  4492  dfif3  4543  dfif5  4545  rabsnif  4728  tpidm  4763  ssunpr  4836  sstp  4838  opidg  4893  dfint2  4953  iunrab  5056  uniiun  5062  intiin  5063  iunid  5064  0iin  5068  mptv  5265  dfepfr  5662  epfrc  5663  xpundi  5745  xpundir  5746  csbcnv  5884  resiun2  6003  resopab  6035  mptresid  6051  dffr3  6099  dfse2  6100  cnvun  6143  imaundir  6151  imainrect  6181  cnvcnv2  6193  cnvrescnv  6195  cnvcnvres  6205  dmtpop  6218  rnsnopg  6221  resdifdi  6236  rnco2  6253  dmco  6254  co01  6261  unidmrn  6279  dfdm2  6281  predidm  6328  tz6.26OLD  6350  dfmpt3  6685  mptun  6697  funcocnv2  6859  dffv2  6987  fnasrn  7143  fpr  7152  fmptap  7168  rnmptc  7208  rnmptcOLD  7209  riotav  7370  dmoprab  7510  rnoprab2  7513  mpov  7520  mpomptx  7521  abrexex2g  7951  1stval2  7992  2ndval2  7993  fo1st  7995  fo2nd  7996  xp2  8012  dfoprab4f  8042  offval22  8074  fmpoco  8081  fimaproj  8121  tposmpo  8248  tposconst  8249  recsfval  8381  rdgsucmpt2  8430  frsucmpt2  8440  df2o3  8474  o1p1e2  8540  o2p2e4  8541  oarec  8562  omopthlem2  8659  ecqs  8775  qliftf  8799  erovlem  8807  fset0  8848  mapsnf1o3  8889  ixp0x  8920  omf1o  9075  xpf1o  9139  mapunen  9146  enp1ilem  9278  pwfiOLD  9347  marypha1lem  9428  marypha2lem4  9433  dfoi  9506  infeq5i  9631  oemapso  9677  cantnflem1  9684  rankelop  9869  leweon  10006  r0weon  10007  kmlem11  10155  dju1dif  10167  ackbij1lem16  10230  cf0  10246  cfsmolem  10265  alephsuc3  10575  fpwwe  10641  canthp1lem1  10647  wuncval2  10742  prlem936  11042  m1p1sr  11087  m1m1sr  11088  dfcnqs  11137  ssxr  11283  mul02lem2  11391  addrid  11394  2p2e4  12347  3p2e5  12363  3p3e6  12364  4p2e6  12365  4p3e7  12366  4p4e8  12367  5p2e7  12368  5p3e8  12369  5p4e9  12370  6p2e8  12371  6p3e9  12372  7p2e9  12373  nnzrab  12590  nn0zrab  12591  dec0u  12698  dec0h  12699  decsuc  12708  decsucc  12718  numma  12721  decma  12728  decmac  12729  decma2c  12730  decadd  12731  decaddc  12732  decmul1c  12742  decmul2c  12743  5p5e10  12748  6p4e10  12749  7p3e10  12752  8p2e10  12757  5t5e25  12780  6t6e36  12785  8t6e48  12796  nn0uz  12864  nnuz  12865  xaddcom  13219  x2times  13278  ioomax  13399  iccmax  13400  ioopos  13401  ioorp  13402  prunioo  13458  fseq1p1m1  13575  fzo13pr  13716  fzo0to2pr  13717  fzo0to3tp  13718  om2uzrdg  13921  fzennn  13933  irec  14165  sq10e99m1  14225  facnn  14235  fac0  14236  faclbnd2  14251  faclbnd4lem1  14253  hashfun  14397  hashbclem  14411  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1lem2  14417  fz1isolem  14422  swrdccatin1  14675  swrdccat3blem  14689  s1co  14784  s2eq2s1eq  14887  s3eqs2s1eq  14889  ofs2  14918  dfid5  14974  dfid6  14975  fsumrev2  15728  fsumparts  15752  fsumiun  15767  isumnn0nn  15788  harmonic  15805  fprod2d  15925  bpoly2  16001  bpoly3  16002  bpoly4  16003  ege2le3  16033  cos1bnd  16130  efieq1re  16142  eirrlem  16147  qnnen  16156  cpnnen  16172  ruclem6  16178  3dvds  16274  pwp1fsum  16334  m1bits  16381  algrp1  16511  phiprmpw  16709  prmreclem4  16852  4sqlem11  16888  4sqlem19  16896  dec5dvds  16997  decsplit1  17015  5prm  17042  7prm  17044  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  strle1  17091  grpbasex  17236  grpplusgx  17237  quslem  17489  xpsrnbas  17517  acsfn1  17605  acsfn2  17607  comfffval2  17645  dfinito2  17953  dftermo2  17954  xpchomfval  18131  xpccofval  18134  1stfval  18143  2ndfval  18146  oduleg  18243  ismgmid  18584  efmndbas  18752  smndex2dnrinv  18796  grpinvfvi  18867  gaorb  19171  elcntr  19194  cntri  19196  cntrsubgnsg  19207  cntrnsg  19208  setsplusg  19214  oppglemOLD  19215  oppgcntr  19232  gsumwrev  19233  symgressbas  19249  symgplusg  19250  symgvalstruct  19264  symgvalstructOLD  19265  symgga  19275  cayleylem1  19280  psgnunilem2  19363  efgval2  19592  efgredlemc  19613  efgcpbllema  19622  frgpnabllem1  19741  gsumzaddlem  19789  mgplemOLD  19992  opprlem  20155  opprlemOLD  20156  oppr0  20163  opprneg  20165  rmodislmod  20540  rmodislmodOLD  20541  rlmscaf  20831  xrsds  20988  gsumfsum  21012  zringunit  21036  cnmsgngrp  21132  psgnfix2  21152  relt  21168  ocv0  21230  thlle  21251  thlleOLD  21252  thlleval  21253  dsmmval2  21291  frlmip  21333  mplbas  21549  mplplusg  21566  mplmulr  21567  mplvsca2  21573  ressmplbas2  21582  ltbwe  21599  evlslem4  21637  psr1bas2  21714  ply1bas  21719  ply1assa  21723  psr1plusg  21744  psr1vsca  21745  psr1mulr  21746  ply1plusg  21747  ply1vsca  21748  ply1mulr  21749  ply1mpl0  21777  ply1mpl1  21779  coe1mul  21792  matgsum  21939  smadiadetglem1  22173  indistpsx  22513  iuncld  22549  tgrest  22663  resstopn  22690  leordtval2  22716  xkouni  23103  ptclsg  23119  ptuncnv  23311  ptunhmeo  23312  alexsubALTlem4  23554  tsmsf1o  23649  ucnimalem  23785  ressxms  24034  uniretop  24279  cnfldtopn  24298  xrtgioo  24322  zcld  24329  icccmp  24341  xrge0gsumle  24349  xrge0tsms  24350  metnrmlem3  24377  fsum2cn  24387  cnmpopc  24444  oprpiece1res1  24467  oprpiece1res2  24468  evth  24475  evth2  24476  om1opn  24552  pi1xfrf  24569  pi1xfrcnv  24573  pi1cof  24575  clsocv  24767  cncmet  24839  cnflduss  24873  rrxprds  24906  ehlbase  24932  ismbl  25043  shftmbl  25055  ioorinv  25093  itg1addlem4  25216  itg1addlem4OLD  25217  itg2cnlem1  25279  itg0  25297  itgss3  25332  ditgneg  25374  limcdif  25393  limciun  25411  dvexp  25470  dvef  25497  dvcnvrelem2  25535  ftc1  25559  aannenlem2  25842  dvradcnv  25933  pserdvlem2  25940  reefgim  25962  cospi  25982  sincos6thpi  26025  tanregt0  26048  dflog2  26069  logfac  26109  dvlog  26159  cxpexp  26176  cxpmul2  26197  cxpsqrt  26211  dvsqrt  26250  dvcnsqrt  26252  cxpcn2  26254  isosctrlem2  26324  1cubrlem  26346  1cubr  26347  quart1lem  26360  atancj  26415  atanlogaddlem  26418  atansopn  26437  leibpilem2  26446  log2cnv  26449  log2ublem3  26453  birthdaylem1  26456  birthdaylem2  26457  birthday  26459  dfarea  26465  lgamgulmlem5  26537  lgambdd  26541  ftalem3  26579  basellem2  26586  ppiprm  26655  ppinprm  26656  chtprm  26657  chtnprm  26658  ppi2  26674  ppi3  26675  ppiub  26707  chtub  26715  bclbnd  26783  bposlem8  26794  lgsdilem  26827  lgsdir2lem2  26829  lgsquadlem2  26884  lgsquad2lem2  26888  2lgsoddprmlem3c  26915  rplogsum  27030  mulog2sumlem2  27038  pnt2  27116  bdayfo  27180  bday0s  27329  bday1s  27332  old1  27370  addsasslem2  27487  negsbdaylem  27530  muls01  27568  istrkg2ld  27711  axsegconlem9  28183  ax5seglem7  28193  iedgedg  28310  uspgrf1oedg  28433  nbgrcl  28592  nbgrnvtx0  28596  rusgrprc  28847  pthsfval  28978  wlkiswwlks2lem4  29126  wlkiswwlks2lem5  29127  clwwlkvbij  29366  konigsbergumgr  29504  ex-pw  29682  ex-xp  29689  ex-rn  29693  nvvop  29862  nvm  29894  cnims  29946  ip0i  30078  ip1ilem  30079  ipdirilem  30082  ipasslem10  30092  h2hva  30227  h2hsm  30228  h2hvs  30230  axhfvadd-zf  30235  axhvcom-zf  30236  axhvass-zf  30237  axhv0cl-zf  30238  axhvaddid-zf  30239  axhfvmul-zf  30240  axhvmulid-zf  30241  axhvmulass-zf  30242  axhvdistr1-zf  30243  axhvdistr2-zf  30244  axhvmul0-zf  30245  axhfi-zf  30246  axhis1-zf  30247  axhis2-zf  30248  axhis3-zf  30249  axhis4-zf  30250  axhcompl-zf  30251  normlem0  30362  normlem1  30363  normlem2  30364  normlem4  30366  normlem9  30371  bcseqi  30373  dfhnorm2  30375  norm3difi  30400  normpari  30407  normpar2i  30409  polid2i  30410  polidi  30411  hhba  30420  hhims  30425  hhims2  30426  hhsssh  30522  hhssims  30527  hhssims2  30528  shsval3i  30641  dfch2  30660  cmcm2i  30846  fh2  30872  qlaxr3i  30889  spansnji  30899  pjcji  30937  ho0val  31003  df0op2  31005  hosd1i  31075  hosd2i  31076  eigorthi  31090  hhlnoi  31153  hhnmoi  31154  hhbloi  31155  bra0  31203  nmop0  31239  nmfn0  31240  lnopeq0lem1  31258  lnopunilem1  31263  lnophmlem2  31270  nmopcoadji  31354  pjhmopidm  31436  cvmdi  31577  cdj3lem3  31691  cdj3lem3b  31693  abrexdomjm  31744  uniin1  31783  uniin2  31784  iundifdifd  31793  iundifdif  31794  mpomptxf  31905  df1stres  31925  df2ndres  31926  intimafv  31932  fcobijfs  31948  resf1o  31955  fpwrelmapffslem  31957  dpval3  32060  dp3mul10  32064  dpadd2  32076  dpmul4  32080  xrslt  32177  xrsclat  32181  xrge0tsmsd  32209  gsumle  32242  cycpmco2lem7  32291  cycpmconjv  32301  cycpmrn  32302  rndrhmcl  32396  xrge0slmod  32463  lsmsnorb2  32502  qusbas2  32517  rlmdim  32694  rgmoddimOLD  32695  circtopn  32817  tpr2rico  32892  xrge0mulc1cn  32921  lmxrge0  32932  esumpfinvallem  33072  esumcocn  33078  hasheuni  33083  esumcvg  33084  rossros  33178  measinblem  33218  aean  33242  sxbrsigalem3  33271  dya2iocival  33272  dya2iocucvr  33283  sxbrsigalem1  33284  sxbrsigalem2  33285  sxbrsigalem5  33287  sxbrsiga  33289  fiunelcarsg  33315  eulerpartlem1  33366  eulerpartgbij  33371  fibp1  33400  coinfliplem  33477  coinflipprob  33478  ballotlemfval  33488  ballotth  33536  sgnneg  33539  plymulx  33559  circlemethhgt  33655  hgt750lem2  33664  bnj1400  33846  bnj66  33871  bnj882  33937  lfuhgr  34108  derang0  34160  subfacp1lem1  34170  subfacp1lem6  34176  kur14lem7  34203  cvmsss2  34265  cvmliftlem8  34283  cvmliftlem10  34285  satfv1lem  34353  msubfval  34515  quad3  34655  bcprod  34708  bccolsum  34709  faclim  34716  pprodcnveq  34855  dfon4  34865  fobigcup  34872  dfiota3  34895  dfrecs2  34922  dfrdg4  34923  dfint3  34924  rankeq1o  35143  refssfne  35243  ssoninhaus  35333  onint1  35334  bj-rababw  35761  bj-inrab3  35809  bj-imdiridlem  36066  dissneq  36222  dffinxpf  36266  finxpreclem4  36275  rabiun  36461  ptrest  36487  poimirlem3  36491  poimirlem4  36492  poimirlem13  36501  poimirlem16  36504  poimirlem22  36510  poimirlem26  36514  poimirlem27  36515  poimirlem30  36518  cnambfre  36536  ftc1anclem8  36568  fnopabco  36591  abrexdom  36598  cncfres  36633  scottexf  37036  scott0f  37037  inres2  37112  dfres4  37162  xrnres  37272  xrnres2  37273  dfcoss2  37283  dfcoss4  37285  1cossres  37299  dmcoss2  37324  1cosscnvxrn  37345  dfeqvrels2  37458  dfcoeleqvrels  37491  redundss3  37498  dffunsALTV5  37557  cdleme3d  39102  cdleme7a  39114  cdleme31sdnN  39258  cdlemk45  39818  420gcd8e4  40871  lcmeprodgcdi  40872  60lcm7e420  40875  420lcm8e840  40876  3lexlogpow5ineq1  40919  3lexlogpow2ineq1  40923  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1p1  40941  2ap1caineq  40961  sticksstones7  40968  sticksstones12a  40973  sticksstones12  40974  imaopab  41050  fmpocos  41056  dfqs2  41059  dfqs3  41060  decaddcom  41196  sumcubes  41211  nn0expgcd  41226  sn-00idlem2  41272  reixi  41295  sum9cubes  41414  mapfzcons  41454  eldioph4b  41549  diophren  41551  pwssplit4  41831  pwfi2f1o  41838  frlmpwfi  41840  mendplusgfval  41927  mendmulrfval  41929  mendvscafval  41932  idomodle  41938  cytpval  41951  arearect  41964  onov0suclim  42024  omabs2  42082  tr3dom  42279  har2o  42297  alephiso2  42309  alephiso3  42310  relintab  42334  dfid7  42363  cnvrcl0  42376  dfrtrcl5  42380  dfrcl3  42426  dfrcl4  42427  comptiunov2i  42457  corcltrcl  42490  neicvgnvo  42866  inductionexd  42906  mnuprdlem2  43032  nznngen  43075  hashnzfz2  43080  lhe4.4ex1a  43088  dvradcnv2  43106  binomcxplemrat  43109  binomcxplemnotnn0  43115  refsum2cnlem1  43721  fiiuncl  43752  iccdifprioo  44229  lptre2pt  44356  limclner  44367  stoweidlem13  44729  stoweidlem32  44748  stoweidlem62  44778  wallispi2lem2  44788  stirlinglem14  44803  dirkertrigeqlem1  44814  dirkercncflem4  44822  fourierdlem42  44865  fourierdlem73  44895  fourierdlem81  44903  fourierdlem92  44914  fourierdlem103  44925  fourierdlem104  44926  fouriercnp  44942  fouriersw  44947  sge0tsms  45096  sge0iunmptlemfi  45129  ovolval5lem3  45370  cnfsmf  45456  rnfdmpr  45989  fvmptrabdm  46001  fundcmpsurinjlem1  46066  m11nprm  46269  opoeALTV  46351  nfermltl8rev  46410  sbgoldbo  46455  evengpop3  46466  pzriprng1  46822  cznabel  46852  cznrng  46853  mpomptx2  47010  2sphere  47435  itscnhlinecirc02plem3  47470  inlinecirc02p  47473  icccldii  47551  dfnrm2  47564  dfnrm3  47565  amgmlemALT  47850