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  27330  bday1s  27333  old1  27371  addsasslem2  27490  negsbdaylem  27533  muls01  27571  istrkg2ld  27742  axsegconlem9  28214  ax5seglem7  28224  iedgedg  28341  uspgrf1oedg  28464  nbgrcl  28623  nbgrnvtx0  28627  rusgrprc  28878  pthsfval  29009  wlkiswwlks2lem4  29157  wlkiswwlks2lem5  29158  clwwlkvbij  29397  konigsbergumgr  29535  ex-pw  29713  ex-xp  29720  ex-rn  29724  nvvop  29893  nvm  29925  cnims  29977  ip0i  30109  ip1ilem  30110  ipdirilem  30113  ipasslem10  30123  h2hva  30258  h2hsm  30259  h2hvs  30261  axhfvadd-zf  30266  axhvcom-zf  30267  axhvass-zf  30268  axhv0cl-zf  30269  axhvaddid-zf  30270  axhfvmul-zf  30271  axhvmulid-zf  30272  axhvmulass-zf  30273  axhvdistr1-zf  30274  axhvdistr2-zf  30275  axhvmul0-zf  30276  axhfi-zf  30277  axhis1-zf  30278  axhis2-zf  30279  axhis3-zf  30280  axhis4-zf  30281  axhcompl-zf  30282  normlem0  30393  normlem1  30394  normlem2  30395  normlem4  30397  normlem9  30402  bcseqi  30404  dfhnorm2  30406  norm3difi  30431  normpari  30438  normpar2i  30440  polid2i  30441  polidi  30442  hhba  30451  hhims  30456  hhims2  30457  hhsssh  30553  hhssims  30558  hhssims2  30559  shsval3i  30672  dfch2  30691  cmcm2i  30877  fh2  30903  qlaxr3i  30920  spansnji  30930  pjcji  30968  ho0val  31034  df0op2  31036  hosd1i  31106  hosd2i  31107  eigorthi  31121  hhlnoi  31184  hhnmoi  31185  hhbloi  31186  bra0  31234  nmop0  31270  nmfn0  31271  lnopeq0lem1  31289  lnopunilem1  31294  lnophmlem2  31301  nmopcoadji  31385  pjhmopidm  31467  cvmdi  31608  cdj3lem3  31722  cdj3lem3b  31724  abrexdomjm  31775  uniin1  31814  uniin2  31815  iundifdifd  31824  iundifdif  31825  mpomptxf  31936  df1stres  31956  df2ndres  31957  intimafv  31963  fcobijfs  31979  resf1o  31986  fpwrelmapffslem  31988  dpval3  32091  dp3mul10  32095  dpadd2  32107  dpmul4  32111  xrslt  32208  xrsclat  32212  xrge0tsmsd  32240  gsumle  32273  cycpmco2lem7  32322  cycpmconjv  32332  cycpmrn  32333  rndrhmcl  32427  xrge0slmod  32494  lsmsnorb2  32533  qusbas2  32548  rlmdim  32725  rgmoddimOLD  32726  circtopn  32848  tpr2rico  32923  xrge0mulc1cn  32952  lmxrge0  32963  esumpfinvallem  33103  esumcocn  33109  hasheuni  33114  esumcvg  33115  rossros  33209  measinblem  33249  aean  33273  sxbrsigalem3  33302  dya2iocival  33303  dya2iocucvr  33314  sxbrsigalem1  33315  sxbrsigalem2  33316  sxbrsigalem5  33318  sxbrsiga  33320  fiunelcarsg  33346  eulerpartlem1  33397  eulerpartgbij  33402  fibp1  33431  coinfliplem  33508  coinflipprob  33509  ballotlemfval  33519  ballotth  33567  sgnneg  33570  plymulx  33590  circlemethhgt  33686  hgt750lem2  33695  bnj1400  33877  bnj66  33902  bnj882  33968  lfuhgr  34139  derang0  34191  subfacp1lem1  34201  subfacp1lem6  34207  kur14lem7  34234  cvmsss2  34296  cvmliftlem8  34314  cvmliftlem10  34316  satfv1lem  34384  msubfval  34546  quad3  34686  bcprod  34739  bccolsum  34740  faclim  34747  pprodcnveq  34886  dfon4  34896  fobigcup  34903  dfiota3  34926  dfrecs2  34953  dfrdg4  34954  dfint3  34955  rankeq1o  35174  refssfne  35291  ssoninhaus  35381  onint1  35382  bj-rababw  35809  bj-inrab3  35857  bj-imdiridlem  36114  dissneq  36270  dffinxpf  36314  finxpreclem4  36323  rabiun  36509  ptrest  36535  poimirlem3  36539  poimirlem4  36540  poimirlem13  36549  poimirlem16  36552  poimirlem22  36558  poimirlem26  36562  poimirlem27  36563  poimirlem30  36566  cnambfre  36584  ftc1anclem8  36616  fnopabco  36639  abrexdom  36646  cncfres  36681  scottexf  37084  scott0f  37085  inres2  37160  dfres4  37210  xrnres  37320  xrnres2  37321  dfcoss2  37331  dfcoss4  37333  1cossres  37347  dmcoss2  37372  1cosscnvxrn  37393  dfeqvrels2  37506  dfcoeleqvrels  37539  redundss3  37546  dffunsALTV5  37605  cdleme3d  39150  cdleme7a  39162  cdleme31sdnN  39306  cdlemk45  39866  420gcd8e4  40919  lcmeprodgcdi  40920  60lcm7e420  40923  420lcm8e840  40924  3lexlogpow5ineq1  40967  3lexlogpow2ineq1  40971  3lexlogpow2ineq2  40972  3lexlogpow5ineq5  40973  aks4d1p1  40989  2ap1caineq  41009  sticksstones7  41016  sticksstones12a  41021  sticksstones12  41022  imaopab  41098  fmpocos  41104  dfqs2  41107  dfqs3  41108  decaddcom  41244  sumcubes  41259  nn0expgcd  41274  sn-00idlem2  41320  reixi  41343  sum9cubes  41462  mapfzcons  41502  eldioph4b  41597  diophren  41599  pwssplit4  41879  pwfi2f1o  41886  frlmpwfi  41888  mendplusgfval  41975  mendmulrfval  41977  mendvscafval  41980  idomodle  41986  cytpval  41999  arearect  42012  onov0suclim  42072  omabs2  42130  tr3dom  42327  har2o  42345  alephiso2  42357  alephiso3  42358  relintab  42382  dfid7  42411  cnvrcl0  42424  dfrtrcl5  42428  dfrcl3  42474  dfrcl4  42475  comptiunov2i  42505  corcltrcl  42538  neicvgnvo  42914  inductionexd  42954  mnuprdlem2  43080  nznngen  43123  hashnzfz2  43128  lhe4.4ex1a  43136  dvradcnv2  43154  binomcxplemrat  43157  binomcxplemnotnn0  43163  refsum2cnlem1  43769  fiiuncl  43800  iccdifprioo  44277  lptre2pt  44404  limclner  44415  stoweidlem13  44777  stoweidlem32  44796  stoweidlem62  44826  wallispi2lem2  44836  stirlinglem14  44851  dirkertrigeqlem1  44862  dirkercncflem4  44870  fourierdlem42  44913  fourierdlem73  44943  fourierdlem81  44951  fourierdlem92  44962  fourierdlem103  44973  fourierdlem104  44974  fouriercnp  44990  fouriersw  44995  sge0tsms  45144  sge0iunmptlemfi  45177  ovolval5lem3  45418  cnfsmf  45504  rnfdmpr  46037  fvmptrabdm  46049  fundcmpsurinjlem1  46114  m11nprm  46317  opoeALTV  46399  nfermltl8rev  46458  sbgoldbo  46503  evengpop3  46514  pzriprng1  46870  cznabel  46900  cznrng  46901  mpomptx2  47058  2sphere  47483  itscnhlinecirc02plem3  47518  inlinecirc02p  47521  icccldii  47599  dfnrm2  47612  dfnrm3  47613  amgmlemALT  47898