Theorem eqtr4i 2789

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  3eqtr2i  2792  3eqtr2ri  2793  3eqtr4i  2796  3eqtr4ri  2797  rabab  3483  cbvralcsf  3892  cbvrabcsf  3895  dfdif2  4050  dfin5  4094  uneqin  4236  notabw  4260  unrab  4262  inrab  4263  inrab2  4264  difrab  4265  dfrab3ss  4270  rabun2  4271  dfnul2  4283  difid  4327  rabxm  4342  elnelun  4345  abf  4366  difdifdir  4449  dfif3  4499  dfif5  4501  rabsnif  4683  tpidm  4718  ssunpr  4791  sstp  4793  opidg  4854  dfint2  4911  iunrab  5013  uniiun  5019  intiin  5020  iunid  5021  0iin  5024  uniin1  5035  uniin2  5036  mptv  5213  dfepfr  5638  epfrc  5639  xpundi  5723  xpundir  5724  csbcnv  5868  csbcnvOLD  5869  resiun2  5995  resopab  6031  mptresid  6048  dffr3  6102  dfse2  6103  cnvun  6138  imaundir  6147  imainrect  6178  cnvcnv2  6190  cnvrescnv  6193  cnvcnvres  6212  dmtpop  6225  rnsnopg  6228  resdifdi  6243  rnco2  6261  dmco  6262  co01  6269  unidmrn  6288  dfdm2  6290  predidm  6335  dfmpt3  6681  mptun  6693  funcocnv2  6858  dffv2  6988  fnasrn  7156  fpr  7166  fmptap  7182  rnmptc  7220  riotav  7389  dmoprab  7530  rnoprab2  7533  mpov  7539  mpomptx  7540  abrexex2g  7983  1stval2  8025  2ndval2  8026  fo1st  8028  fo2nd  8029  xp2  8045  dfoprab4f  8075  offval22  8107  fmpoco  8115  fimaproj  8162  tposmpo  8291  tposconst  8292  recsfval  8399  rdgsucmpt2  8449  frsucmpt2  8459  df2o3  8495  o1p1e2  8559  o2p2e4  8560  oarec  8581  omopthlem2  8680  dfqs2  8735  ecqs  8811  qliftf  8837  erovlem  8845  fset0  8887  mapsnf1o3  8934  ixp0x  8965  omf1o  9110  xpf1o  9169  mapunen  9176  enp1ilem  9280  marypha1lem  9435  marypha2lem4  9440  dfoi  9515  infeq5i  9647  oemapso  9693  cantnflem1  9700  rankelop  9901  leweon  10100  r0weon  10101  kmlem11  10249  dju1dif  10261  ackbij1lem16  10322  cf0  10338  cfsmolem  10358  alephsuc3  10675  fpwwe  10741  canthp1lem1  10747  wuncval2  10842  prlem936  11142  m1p1sr  11187  m1m1sr  11188  dfcnqs  11237  ssxr  11389  mul02lem2  11497  addrid  11500  2p2e4  12487  3p2e5  12503  3p3e6  12504  4p2e6  12505  4p3e7  12506  4p4e8  12507  5p2e7  12508  5p3e8  12509  5p4e9  12510  6p2e8  12511  6p3e9  12512  7p2e9  12513  nnzrab  12734  nn0zrab  12735  dec0u  12850  dec0h  12851  decsuc  12860  decsucc  12870  numma  12873  decma  12880  decmac  12881  decma2c  12882  decadd  12883  decaddc  12884  decmul1c  12894  decmul2c  12895  5p5e10  12900  6p4e10  12901  7p3e10  12904  8p2e10  12909  5t5e25  12932  6t6e36  12937  8t6e48  12948  nn0uz  13013  nnuz  13014  xaddcom  13380  x2times  13439  ioomax  13563  iccmax  13564  ioopos  13565  ioorp  13566  prunioo  13622  fseq1p1m1  13742  fzo13pr  13894  fzo0to2pr  13895  fzo0to3tp  13897  om2uzrdg  14109  fzennn  14121  irec  14355  sq10e99m1  14419  facnn  14429  fac0  14430  faclbnd2  14445  faclbnd4lem1  14447  hashfun  14592  hashbclem  14607  hashf1lem1  14610  hashf1lem2  14611  fz1isolem  14616  swrdccatin1  14885  swrdccat3blem  14899  s1co  14995  s2eq2s1eq  15099  s3eqs2s1eq  15101  ofs2  15136  dfid5  15192  dfid6  15193  sgnneg  15265  fsumrev2  15960  fsumparts  15985  fsumiun  16000  isumnn0nn  16023  harmonic  16040  fprod2d  16160  bpoly2  16235  bpoly3  16236  bpoly4  16237  ege2le3  16268  cos1bnd  16367  efieq1re  16379  eirrlem  16384  qnnen  16393  cpnnen  16409  ruclem6  16415  3dvds  16513  pwp1fsum  16573  m1bits  16622  nn0expgcd  16750  algrp1  16761  phiprmpw  16965  prmreclem4  17109  4sqlem11  17145  4sqlem19  17153  dec5dvds  17254  decsplit1  17271  5prm  17298  7prm  17300  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  1259prm  17326  2503lem1  17327  2503lem2  17328  2503lem3  17329  2503prm  17330  4001lem1  17331  4001lem2  17332  4001lem3  17333  4001lem4  17334  4001prm  17335  strle1  17348  grpbasex  17475  grpplusgx  17476  quslem  17727  xpsrnbas  17755  acsfn1  17847  acsfn2  17849  comfffval2  17887  dfinito2  18190  dftermo2  18191  xpchomfval  18365  xpccofval  18368  1stfval  18377  2ndfval  18380  oduleg  18476  chnub  18808  idvalriota  18853  ismgmid  18857  efmndbas  19079  smndex2dnrinv  19126  degenmgmbas  19147  degenmgm2opdm  19150  grpinvfvi  19205  gaorb  19533  elcntr  19556  cntri  19558  cntrsubgnsg  19569  cntrnsg  19570  setsplusg  19576  oppgcntr  19591  gsumwrev  19592  symgressbas  19608  symgplusg  19609  symgvalstruct  19623  symgga  19633  cayleylem1  19638  psgnunilem2  19721  efgval2  19950  efgredlemc  19971  efgcpbllema  19980  frgpnabllem1  20099  gsumzaddlem  20147  gsumle  20371  opprlem  20584  oppr0  20591  opprneg  20593  rmodislmod  21217  rlmscaf  21494  xrsds  21728  gsumfsum  21752  zringunit  21784  pzriprng1  21816  cnmsgngrp  21897  psgnfix2  21917  relt  21933  ocv0  21995  thlle  22015  thlleval  22016  dsmmval2  22054  frlmip  22096  mplbas  22309  mplplusg  22326  mplmulr  22327  mplvsca2  22333  ressmplbas2  22347  ltbwe  22365  evlslem4  22397  psdmul  22499  psr1bas2  22520  ply1bas  22525  ply1assa  22529  psr1plusg  22550  psr1vsca  22551  psr1mulr  22552  ply1plusg  22553  ply1vsca  22554  ply1mulr  22555  ply1mpl0  22586  ply1mpl1  22588  coe1mul  22601  matgsum  22764  smadiadetglem1  22998  indistpsx  23340  iuncld  23375  tgrest  23489  resstopn  23516  leordtval2  23542  xkouni  23930  ptclsg  23946  ptuncnv  24138  ptunhmeo  24139  alexsubALTlem4  24381  tsmsf1o  24476  ucnimalem  24610  ressxms  24856  uniretop  25093  cnfldtopn  25112  xrtgioo  25138  zcld  25145  icccmp  25157  xrge0gsumle  25165  xrge0tsms  25166  metnrmlem3  25193  fsum2cn  25204  cnmpopc  25261  oprpiece1res1  25284  oprpiece1res2  25285  evth  25292  evth2  25293  om1opn  25369  pi1xfrf  25386  pi1xfrcnv  25390  pi1cof  25392  clsocv  25583  cncmet  25655  cnflduss  25689  rrxprds  25722  ehlbase  25748  ehl2eudis  25755  ismbl  25859  shftmbl  25871  ioorinv  25909  itg1addlem4  26032  itg2cnlem1  26094  itg0  26112  itgss3  26147  ditgneg  26189  limcdif  26208  limciun  26226  dvexp  26285  dvef  26312  dvcnvrelem2  26350  ftc1  26374  plymulidp  26615  aannenlem2  26668  dvradcnv  26760  pserdvlem2  26767  reefgim  26789  cospi  26813  sincos6thpi  26856  tanregt0  26879  dflog2  26900  logfac  26941  dvlog  26991  cxpexp  27008  cxpmul2  27029  cxpsqrt  27043  dvsqrt  27082  dvcnsqrt  27084  cxpcn2  27086  isosctrlem2  27159  1cubrlem  27181  1cubr  27182  quart1lem  27195  atancj  27250  atanlogaddlem  27253  atansopn  27272  leibpilem2  27281  log2cnv  27284  log2ublem3  27288  birthdaylem1  27291  birthdaylem2  27292  birthday  27294  dfarea  27300  lgamgulmlem5  27372  lgambdd  27376  ftalem3  27414  basellem2  27421  ppiprm  27490  ppinprm  27491  chtprm  27492  chtnprm  27493  ppi2  27509  ppi3  27510  ppiub  27543  chtub  27551  bclbnd  27619  bposlem8  27630  lgsdilem  27663  lgsdir2lem2  27665  lgsquadlem2  27720  lgsquad2lem2  27724  2lgsoddprmlem3c  27751  rplogsum  27866  mulog2sumlem2  27874  pnt2  27952  fltoprmlem2  28006  bdayfo  28046  bday0  28209  bday1  28212  old1  28263  addsasslem2  28402  negbdaylem  28454  muls01  28510  abssnid  28641  1p1e2s  28814  n0seo  28819  twocut  28821  halfcut  28856  pw2cutp1  28859  pw2cut2  28860  istrkg2ld  28934  axsegconlem9  29515  ax5seglem7  29525  iedgedg  29640  lfuhgr  29738  uspgrf1oedg  29766  nbgrcl  29928  nbgrnvtx0  29932  rusgrprc  30183  pthsfval  30316  wlkiswwlks2lem4  30473  wlkiswwlks2lem5  30474  clwwlkvbij  30716  konigsbergumgr  30864  ex-pw  31042  ex-xp  31049  ex-rn  31053  nvvop  31223  nvm  31255  cnims  31307  ip0i  31439  ip1ilem  31440  ipdirilem  31443  ipasslem10  31453  h2hva  31588  h2hsm  31589  h2hvs  31591  axhfvadd-zf  31596  axhvcom-zf  31597  axhvass-zf  31598  axhv0cl-zf  31599  axhvaddid-zf  31600  axhfvmul-zf  31601  axhvmulid-zf  31602  axhvmulass-zf  31603  axhvdistr1-zf  31604  axhvdistr2-zf  31605  axhvmul0-zf  31606  axhfi-zf  31607  axhis1-zf  31608  axhis2-zf  31609  axhis3-zf  31610  axhis4-zf  31611  axhcompl-zf  31612  normlem0  31723  normlem1  31724  normlem2  31725  normlem4  31727  normlem9  31732  bcseqi  31734  dfhnorm2  31736  norm3difi  31761  normpari  31768  normpar2i  31770  polid2i  31771  polidi  31772  hhba  31781  hhims  31786  hhims2  31787  hhsssh  31883  hhssims  31888  hhssims2  31889  shsval3i  32002  dfch2  32021  cmcm2i  32207  fh2  32233  qlaxr3i  32250  spansnji  32260  pjcji  32298  ho0val  32364  df0op2  32366  hosd1i  32436  hosd2i  32437  eigorthi  32451  hhlnoi  32514  hhnmoi  32515  hhbloi  32516  bra0  32564  nmop0  32600  nmfn0  32601  lnopeq0lem1  32619  lnopunilem1  32624  lnophmlem2  32631  nmopcoadji  32715  pjhmopidm  32797  cvmdi  32938  cdj3lem3  33052  cdj3lem3b  33054  abrexdomjm  33157  iundifdifd  33210  iundifdif  33211  mpomptxf  33326  df1stres  33351  df2ndres  33352  intimafv  33358  fcobijfs  33366  fcobijfs2  33367  resf1o  33375  fpwrelmapffslem  33377  dpval3  33513  dp3mul10  33517  dpadd2  33529  dpmul4  33533  ccatws1f1o  33567  xrslt  33621  xrsclat  33625  xrge0tsmsd  33687  cycpmco2lem7  33746  cycpmconjv  33756  cycpmrn  33757  conjga  33784  elrgspnsubrunlem2  33862  rndrhmcl  33911  fracf1  33922  xrge0slmod  33962  lsmsnorb2  34000  qusbas2  34010  1arithidomlem2  34121  zringfrac  34139  selvply1rhm0  34211  mplvrpmga  34230  mplvrpmmhm  34231  mplvrpmrhm  34232  psrmonprod  34237  mplmonprod  34239  vieta  34265  rlmdim  34295  isconstr  34421  iconstr  34451  cos9thpiminplylem4  34470  cos9thpiminplylem5  34471  circtopn  34522  tpr2rico  34597  xrge0mulc1cn  34626  lmxrge0  34637  esumpfinvallem  34759  esumcocn  34765  hasheuni  34770  esumcvg  34771  rossros  34866  measinblem  34906  aean  34930  sxbrsigalem3  34957  dya2iocival  34958  dya2iocucvr  34969  sxbrsigalem1  34970  sxbrsigalem2  34971  sxbrsigalem5  34973  sxbrsiga  34975  fiunelcarsg  35001  eulerpartlem1  35052  eulerpartgbij  35057  fibp1  35086  coinfliplem  35164  coinflipprob  35165  ballotlemfval  35175  ballotth  35223  circlemethhgt  35325  hgt750lem2  35334  bnj1400  35518  bnj66  35543  bnj882  35609  onf1we  35780  werankwe  35800  werankwe2  35801  dfscott2  35805  dfscott3  35806  dfj2  35963  derang0  36055  subfacp1lem1  36065  subfacp1lem6  36071  kur14lem7  36098  cvmsss2  36160  cvmliftlem8  36178  cvmliftlem10  36180  satfv1lem  36248  msubfval  36410  quad3  36556  mirimanoff  36582  onprcALT  36584  bcprod  36630  bccolsum  36631  faclim  36638  pprodcnveq  36772  dfon4  36782  fobigcup  36789  dfiota3  36812  dfrecs2  36841  dfrdg4  36842  dfint3  36843  rankeq1o  37059  refssfne  37273  ssoninhaus  37363  onint1  37364  ttciun  37429  bj-dfnul2  37567  bj-rababw  37920  bj-inrab3  37969  bj-cnvcnv2  38096  bj-imdiridlem  38246  dissneq  38404  dffinxpf  38448  finxpreclem4  38457  rabiun  38661  ptrest  38677  poimirlem3  38681  poimirlem4  38682  poimirlem13  38691  poimirlem16  38694  poimirlem22  38700  poimirlem26  38704  poimirlem27  38705  poimirlem30  38708  cnambfre  38726  ftc1anclem8  38758  fnopabco  38797  abrexdom  38804  cncfres  38839  scottexf  39240  scott0f  39241  inres2  39319  eqrabi  39328  xpv  39334  dfres4  39371  dmxrn  39459  xrnres  39497  xrnres2  39498  rnqmap  39526  dfsucmap2  39536  dfcoss2  39575  dfcoss4  39577  1cossres  39591  dmcoss2  39616  1cosscnvxrn  39637  dfeqvrels2  39744  dfcoeleqvrels  39777  redundss3  39784  dffunsALTV5  39844  dfpeters2  40046  cdleme3d  41428  cdleme7a  41440  cdleme31sdnN  41584  cdlemk45  42144  420gcd8e4  43196  lcmeprodgcdi  43197  60lcm7e420  43200  420lcm8e840  43201  3lexlogpow5ineq1  43244  3lexlogpow2ineq1  43248  3lexlogpow2ineq2  43249  3lexlogpow5ineq5  43250  aks4d1p1  43266  posbezout  43290  aks6d1c1p4  43301  aks6d1c3  43313  2ap1caineq  43335  sticksstones7  43342  sticksstones12a  43347  sticksstones12  43348  aks6d1c6lem4  43363  25or6to4  43396  imaopab  43425  fmpocos  43427  dfqs3  43430  decaddcom  43481  sumcubes  43510  redvmptabs  43551  readvrec  43553  readvcot  43555  sn-00idlem2  43590  reixi  43614  sum9cubes  43823  mapfzcons  43867  eldioph4b  43958  diophren  43960  pwssplit4  44231  pwfi2f1o  44238  frlmpwfi  44240  mendplusgfval  44323  mendmulrfval  44325  mendvscafval  44328  idomodle  44333  cytpval  44344  arearect  44357  onov0suclim  44416  omabs2  44474  tr3dom  44669  har2o  44687  alephiso2  44699  alephiso3  44700  relintab  44724  dfid7  44752  cnvrcl0  44765  dfrtrcl5  44769  dfrcl3  44815  dfrcl4  44816  comptiunov2i  44846  corcltrcl  44879  neicvgnvo  45255  inductionexd  45295  mnuprdlem2  45397  nznngen  45440  hashnzfz2  45445  lhe4.4ex1a  45453  dvradcnv2  45471  binomcxplemrat  45474  binomcxplemnotnn0  45480  nregmodelf1o  46144  refsum2cnlem1  46193  fiiuncl  46221  iccdifprioo  46667  lptre2pt  46789  limclner  46800  stoweidlem13  47162  stoweidlem32  47181  stoweidlem62  47211  wallispi2lem2  47221  stirlinglem14  47236  dirkertrigeqlem1  47247  dirkercncflem4  47255  fourierdlem42  47298  fourierdlem73  47328  fourierdlem81  47336  fourierdlem92  47347  fourierdlem103  47358  fourierdlem104  47359  fouriercnp  47375  fouriersw  47380  sge0tsms  47529  sge0iunmptlemfi  47562  ovolval5lem3  47803  cnfsmf  47889  goldpolyfactor  48066  goldratval  48075  lamberte  48077  rnfdmpr  48490  fvmptrabdm  48502  fundcmpsurinjlem1  48619  m11nprm  48825  ppi1sum  48855  opoeALTV  48920  nfermltl8rev  48979  sbgoldbo  49024  evengpop3  49035  clnbgrcl  49058  clnbgrnvtx0  49064  usgrexmpl2edg  49266  usgrexmpl2nb0  49268  usgrexmpl2nb3  49271  gpg5order  49297  gpgprismgr4cycllem6  49337  cznabel  49496  cznrng  49497  mpomptx2  49586  inlinecirc02p  50038  dftpos5  50126  tposresg  50130  icccldii  50172  dfnrm2  50185  dfnrm3  50186  elxpcbasex1ALT  50510  elxpcbasex2ALT  50512  dfswapf2  50522  swapf1a  50530  swapf1f1o  50536  swapf2f1oa  50538  swapfida  50541  setc1oterm  50765  setc1ohomfval  50767  setc1ocofval  50768  funcsetc1o  50771  dfinito4  50775  setc1onsubc  50879  islmd  50987  iscmd  50988  initocmd  50991  termolmd  50992  dvsec  51070  dvcsc  51071  dvcot  51072  amgmlemALT  51202