Theorem eqtr4i 2755

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  3eqtr2i  2758  3eqtr2ri  2759  3eqtr4i  2762  3eqtr4ri  2763  rabab  3475  cbvralcsf  3901  cbvrabcsf  3904  dfin5  3919  dfdif2  3920  uneqin  4248  notabw  4272  unrab  4274  inrab  4275  inrab2  4276  difrab  4277  dfrab3ss  4282  rabun2  4283  dfnul2  4295  difid  4335  rabxm  4349  elnelun  4352  abf  4365  difdifdir  4451  dfif3  4499  dfif5  4501  rabsnif  4683  tpidm  4718  ssunpr  4794  sstp  4796  opidg  4852  dfint2  4908  iunrab  5011  uniiun  5017  intiin  5018  iunid  5019  0iin  5023  mptv  5208  dfepfr  5615  epfrc  5616  xpundi  5700  xpundir  5701  csbcnv  5837  resiun2  5960  resopab  5994  mptresid  6011  dffr3  6059  dfse2  6060  cnvun  6103  imaundir  6111  imainrect  6142  cnvcnv2  6154  cnvrescnv  6156  cnvcnvres  6166  dmtpop  6179  rnsnopg  6182  resdifdi  6197  rnco2  6214  dmco  6215  co01  6222  unidmrn  6240  dfdm2  6242  predidm  6287  dfmpt3  6634  mptun  6646  funcocnv2  6807  dffv2  6938  fnasrn  7099  fpr  7108  fmptap  7126  rnmptc  7163  riotav  7331  dmoprab  7472  rnoprab2  7475  mpov  7481  mpomptx  7482  abrexex2g  7922  1stval2  7964  2ndval2  7965  fo1st  7967  fo2nd  7968  xp2  7984  dfoprab4f  8014  offval22  8044  fmpoco  8051  fimaproj  8091  tposmpo  8219  tposconst  8220  recsfval  8326  rdgsucmpt2  8375  frsucmpt2  8385  df2o3  8419  o1p1e2  8481  o2p2e4  8482  oarec  8503  omopthlem2  8601  ecqs  8729  qliftf  8755  erovlem  8763  fset0  8804  mapsnf1o3  8845  ixp0x  8876  omf1o  9021  xpf1o  9080  mapunen  9087  enp1ilem  9199  marypha1lem  9360  marypha2lem4  9365  dfoi  9440  infeq5i  9565  oemapso  9611  cantnflem1  9618  rankelop  9803  leweon  9940  r0weon  9941  kmlem11  10090  dju1dif  10102  ackbij1lem16  10163  cf0  10180  cfsmolem  10199  alephsuc3  10509  fpwwe  10575  canthp1lem1  10581  wuncval2  10676  prlem936  10976  m1p1sr  11021  m1m1sr  11022  dfcnqs  11071  ssxr  11219  mul02lem2  11327  addrid  11330  2p2e4  12292  3p2e5  12308  3p3e6  12309  4p2e6  12310  4p3e7  12311  4p4e8  12312  5p2e7  12313  5p3e8  12314  5p4e9  12315  6p2e8  12316  6p3e9  12317  7p2e9  12318  nnzrab  12537  nn0zrab  12538  dec0u  12646  dec0h  12647  decsuc  12656  decsucc  12666  numma  12669  decma  12676  decmac  12677  decma2c  12678  decadd  12679  decaddc  12680  decmul1c  12690  decmul2c  12691  5p5e10  12696  6p4e10  12697  7p3e10  12700  8p2e10  12705  5t5e25  12728  6t6e36  12733  8t6e48  12744  nn0uz  12811  nnuz  12812  xaddcom  13176  x2times  13235  ioomax  13359  iccmax  13360  ioopos  13361  ioorp  13362  prunioo  13418  fseq1p1m1  13535  fzo13pr  13686  fzo0to2pr  13687  fzo0to3tp  13689  om2uzrdg  13897  fzennn  13909  irec  14142  sq10e99m1  14206  facnn  14216  fac0  14217  faclbnd2  14232  faclbnd4lem1  14234  hashfun  14378  hashbclem  14393  hashf1lem1  14396  hashf1lem2  14397  fz1isolem  14402  swrdccatin1  14666  swrdccat3blem  14680  s1co  14775  s2eq2s1eq  14878  s3eqs2s1eq  14880  ofs2  14913  dfid5  14969  dfid6  14970  fsumrev2  15724  fsumparts  15748  fsumiun  15763  isumnn0nn  15784  harmonic  15801  fprod2d  15923  bpoly2  15999  bpoly3  16000  bpoly4  16001  ege2le3  16032  cos1bnd  16131  efieq1re  16143  eirrlem  16148  qnnen  16157  cpnnen  16173  ruclem6  16179  3dvds  16277  pwp1fsum  16337  m1bits  16386  nn0expgcd  16510  algrp1  16520  phiprmpw  16722  prmreclem4  16866  4sqlem11  16902  4sqlem19  16910  dec5dvds  17011  decsplit1  17028  5prm  17055  7prm  17057  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  strle1  17104  grpbasex  17231  grpplusgx  17232  quslem  17482  xpsrnbas  17510  acsfn1  17602  acsfn2  17604  comfffval2  17642  dfinito2  17945  dftermo2  17946  xpchomfval  18120  xpccofval  18123  1stfval  18132  2ndfval  18135  oduleg  18231  ismgmid  18574  efmndbas  18780  smndex2dnrinv  18824  grpinvfvi  18896  gaorb  19221  elcntr  19244  cntri  19246  cntrsubgnsg  19257  cntrnsg  19258  setsplusg  19264  oppgcntr  19279  gsumwrev  19280  symgressbas  19296  symgplusg  19297  symgvalstruct  19311  symgga  19321  cayleylem1  19326  psgnunilem2  19409  efgval2  19638  efgredlemc  19659  efgcpbllema  19668  frgpnabllem1  19787  gsumzaddlem  19835  gsumle  20059  opprlem  20262  oppr0  20269  opprneg  20271  rmodislmod  20868  rlmscaf  21146  xrsds  21351  gsumfsum  21376  zringunit  21408  pzriprng1  21440  cnmsgngrp  21521  psgnfix2  21541  relt  21557  ocv0  21619  thlle  21639  thlleval  21640  dsmmval2  21678  frlmip  21720  mplbas  21932  mplplusg  21949  mplmulr  21950  mplvsca2  21956  ressmplbas2  21967  ltbwe  21984  evlslem4  22016  psdmul  22086  psr1bas2  22107  ply1bas  22112  ply1basOLD  22113  ply1assa  22117  psr1plusg  22138  psr1vsca  22139  psr1mulr  22140  ply1plusg  22141  ply1vsca  22142  ply1mulr  22143  ply1mpl0  22174  ply1mpl1  22176  coe1mul  22189  matgsum  22357  smadiadetglem1  22591  indistpsx  22930  iuncld  22965  tgrest  23079  resstopn  23106  leordtval2  23132  xkouni  23519  ptclsg  23535  ptuncnv  23727  ptunhmeo  23728  alexsubALTlem4  23970  tsmsf1o  24065  ucnimalem  24200  ressxms  24446  uniretop  24683  cnfldtopn  24702  xrtgioo  24728  zcld  24735  icccmp  24747  xrge0gsumle  24755  xrge0tsms  24756  metnrmlem3  24783  fsum2cn  24795  cnmpopc  24855  oprpiece1res1  24882  oprpiece1res2  24883  evth  24891  evth2  24892  om1opn  24969  pi1xfrf  24986  pi1xfrcnv  24990  pi1cof  24992  clsocv  25183  cncmet  25255  cnflduss  25289  rrxprds  25322  ehlbase  25348  ismbl  25460  shftmbl  25472  ioorinv  25510  itg1addlem4  25633  itg2cnlem1  25695  itg0  25714  itgss3  25749  ditgneg  25791  limcdif  25810  limciun  25828  dvexp  25890  dvef  25917  dvcnvrelem2  25956  ftc1  25982  aannenlem2  26270  dvradcnv  26363  pserdvlem2  26371  reefgim  26393  cospi  26414  sincos6thpi  26458  tanregt0  26481  dflog2  26502  logfac  26543  dvlog  26593  cxpexp  26610  cxpmul2  26631  cxpsqrt  26645  dvsqrt  26684  dvcnsqrt  26686  cxpcn2  26689  isosctrlem2  26762  1cubrlem  26784  1cubr  26785  quart1lem  26798  atancj  26853  atanlogaddlem  26856  atansopn  26875  leibpilem2  26884  log2cnv  26887  log2ublem3  26891  birthdaylem1  26894  birthdaylem2  26895  birthday  26897  dfarea  26903  lgamgulmlem5  26976  lgambdd  26980  ftalem3  27018  basellem2  27025  ppiprm  27094  ppinprm  27095  chtprm  27096  chtnprm  27097  ppi2  27113  ppi3  27114  ppiub  27148  chtub  27156  bclbnd  27224  bposlem8  27235  lgsdilem  27268  lgsdir2lem2  27270  lgsquadlem2  27325  lgsquad2lem2  27329  2lgsoddprmlem3c  27356  rplogsum  27471  mulog2sumlem2  27479  pnt2  27557  bdayfo  27622  bday0s  27777  bday1s  27780  old1  27824  addsasslem2  27951  negsbdaylem  28002  muls01  28055  abssnid  28185  1p1e2s  28343  n0seo  28348  twocut  28350  halfcut  28381  pw2cutp1  28384  zs12bday  28396  istrkg2ld  28440  axsegconlem9  28905  ax5seglem7  28915  iedgedg  29030  uspgrf1oedg  29153  nbgrcl  29315  nbgrnvtx0  29319  rusgrprc  29571  pthsfval  29699  wlkiswwlks2lem4  29852  wlkiswwlks2lem5  29853  clwwlkvbij  30092  konigsbergumgr  30230  ex-pw  30408  ex-xp  30415  ex-rn  30419  nvvop  30588  nvm  30620  cnims  30672  ip0i  30804  ip1ilem  30805  ipdirilem  30808  ipasslem10  30818  h2hva  30953  h2hsm  30954  h2hvs  30956  axhfvadd-zf  30961  axhvcom-zf  30962  axhvass-zf  30963  axhv0cl-zf  30964  axhvaddid-zf  30965  axhfvmul-zf  30966  axhvmulid-zf  30967  axhvmulass-zf  30968  axhvdistr1-zf  30969  axhvdistr2-zf  30970  axhvmul0-zf  30971  axhfi-zf  30972  axhis1-zf  30973  axhis2-zf  30974  axhis3-zf  30975  axhis4-zf  30976  axhcompl-zf  30977  normlem0  31088  normlem1  31089  normlem2  31090  normlem4  31092  normlem9  31097  bcseqi  31099  dfhnorm2  31101  norm3difi  31126  normpari  31133  normpar2i  31135  polid2i  31136  polidi  31137  hhba  31146  hhims  31151  hhims2  31152  hhsssh  31248  hhssims  31253  hhssims2  31254  shsval3i  31367  dfch2  31386  cmcm2i  31572  fh2  31598  qlaxr3i  31615  spansnji  31625  pjcji  31663  ho0val  31729  df0op2  31731  hosd1i  31801  hosd2i  31802  eigorthi  31816  hhlnoi  31879  hhnmoi  31880  hhbloi  31881  bra0  31929  nmop0  31965  nmfn0  31966  lnopeq0lem1  31984  lnopunilem1  31989  lnophmlem2  31996  nmopcoadji  32080  pjhmopidm  32162  cvmdi  32303  cdj3lem3  32417  cdj3lem3b  32419  abrexdomjm  32486  uniin1  32530  uniin2  32531  iundifdifd  32540  iundifdif  32541  mpomptxf  32651  df1stres  32677  df2ndres  32678  intimafv  32684  fcobijfs  32696  resf1o  32703  fpwrelmapffslem  32705  sgnneg  32808  dpval3  32864  dp3mul10  32868  dpadd2  32880  dpmul4  32884  ccatws1f1o  32923  chnub  32984  xrslt  32991  xrsclat  32995  xrge0tsmsd  33045  cycpmco2lem7  33104  cycpmconjv  33114  cycpmrn  33115  conjga  33142  elrgspnsubrunlem2  33215  rndrhmcl  33262  fracf1  33273  xrge0slmod  33312  lsmsnorb2  33356  qusbas2  33370  1arithidomlem2  33500  zringfrac  33518  rlmdim  33598  rgmoddimOLD  33599  isconstr  33719  iconstr  33749  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  circtopn  33820  tpr2rico  33895  xrge0mulc1cn  33924  lmxrge0  33935  esumpfinvallem  34057  esumcocn  34063  hasheuni  34068  esumcvg  34069  rossros  34163  measinblem  34203  aean  34227  sxbrsigalem3  34256  dya2iocival  34257  dya2iocucvr  34268  sxbrsigalem1  34269  sxbrsigalem2  34270  sxbrsigalem5  34272  sxbrsiga  34274  fiunelcarsg  34300  eulerpartlem1  34351  eulerpartgbij  34356  fibp1  34385  coinfliplem  34463  coinflipprob  34464  ballotlemfval  34474  ballotth  34522  plymulx  34532  circlemethhgt  34627  hgt750lem2  34636  bnj1400  34818  bnj66  34843  bnj882  34909  lfuhgr  35098  derang0  35149  subfacp1lem1  35159  subfacp1lem6  35165  kur14lem7  35192  cvmsss2  35254  cvmliftlem8  35272  cvmliftlem10  35274  satfv1lem  35342  msubfval  35504  quad3  35650  bcprod  35718  bccolsum  35719  faclim  35726  pprodcnveq  35864  dfon4  35874  fobigcup  35881  dfiota3  35904  dfrecs2  35931  dfrdg4  35932  dfint3  35933  rankeq1o  36152  refssfne  36339  ssoninhaus  36429  onint1  36430  bj-rababw  36862  bj-inrab3  36910  bj-imdiridlem  37166  dissneq  37322  dffinxpf  37366  finxpreclem4  37375  rabiun  37580  ptrest  37606  poimirlem3  37610  poimirlem4  37611  poimirlem13  37620  poimirlem16  37623  poimirlem22  37629  poimirlem26  37633  poimirlem27  37634  poimirlem30  37637  cnambfre  37655  ftc1anclem8  37687  fnopabco  37710  abrexdom  37717  cncfres  37752  scottexf  38155  scott0f  38156  inres2  38227  dfres4  38274  dmxrn  38353  xrnres  38381  xrnres2  38382  dfcoss2  38397  dfcoss4  38399  1cossres  38413  dmcoss2  38438  1cosscnvxrn  38459  dfeqvrels2  38572  dfcoeleqvrels  38605  redundss3  38612  dffunsALTV5  38672  cdleme3d  40218  cdleme7a  40230  cdleme31sdnN  40374  cdlemk45  40934  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  42212  fmpocos  42215  dfqs2  42218  dfqs3  42219  decaddcom  42265  sumcubes  42294  redvmptabs  42341  readvrec  42343  readvcot  42345  sn-00idlem2  42380  reixi  42404  sum9cubes  42653  mapfzcons  42697  eldioph4b  42792  diophren  42794  pwssplit4  43071  pwfi2f1o  43078  frlmpwfi  43080  mendplusgfval  43163  mendmulrfval  43165  mendvscafval  43168  idomodle  43173  cytpval  43184  arearect  43197  onov0suclim  43256  omabs2  43314  tr3dom  43510  har2o  43528  alephiso2  43540  alephiso3  43541  relintab  43565  dfid7  43594  cnvrcl0  43607  dfrtrcl5  43611  dfrcl3  43657  dfrcl4  43658  comptiunov2i  43688  corcltrcl  43721  neicvgnvo  44097  inductionexd  44137  mnuprdlem2  44255  nznngen  44298  hashnzfz2  44303  lhe4.4ex1a  44311  dvradcnv2  44329  binomcxplemrat  44332  binomcxplemnotnn0  44338  nregmodelf1o  44998  refsum2cnlem1  45024  fiiuncl  45052  iccdifprioo  45507  lptre2pt  45631  limclner  45642  stoweidlem13  46004  stoweidlem32  46023  stoweidlem62  46053  wallispi2lem2  46063  stirlinglem14  46078  dirkertrigeqlem1  46089  dirkercncflem4  46097  fourierdlem42  46140  fourierdlem73  46170  fourierdlem81  46178  fourierdlem92  46189  fourierdlem103  46200  fourierdlem104  46201  fouriercnp  46217  fouriersw  46222  sge0tsms  46371  sge0iunmptlemfi  46404  ovolval5lem3  46645  cnfsmf  46731  lamberte  46882  rnfdmpr  47275  fvmptrabdm  47287  fundcmpsurinjlem1  47392  m11nprm  47595  opoeALTV  47677  nfermltl8rev  47736  sbgoldbo  47781  evengpop3  47792  clnbgrcl  47815  clnbgrnvtx0  47821  usgrexmpl2edg  48013  usgrexmpl2nb0  48015  usgrexmpl2nb3  48018  gpg5order  48044  gpgprismgr4cycllem6  48083  cznabel  48241  cznrng  48242  mpomptx2  48316  2sphere  48731  itscnhlinecirc02plem3  48766  inlinecirc02p  48769  dftpos5  48855  tposresg  48859  icccldii  48900  dfnrm2  48913  dfnrm3  48914  elxpcbasex1ALT  49231  elxpcbasex2ALT  49233  dfswapf2  49243  swapf1a  49251  swapf1f1o  49257  swapf2f1oa  49259  swapfida  49262  setc1oterm  49473  setc1ohomfval  49475  setc1ocofval  49476  funcsetc1o  49479  dfinito4  49483  setc1onsubc  49584  islmd  49647  iscmd  49648  initocmd  49651  termolmd  49652  amgmlemALT  49785