Theorem eqtr4i 2757

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  3eqtr2i  2760  3eqtr2ri  2761  3eqtr4i  2764  3eqtr4ri  2765  rabab  3467  cbvralcsf  3887  cbvrabcsf  3890  dfin5  3905  dfdif2  3906  uneqin  4236  notabw  4260  unrab  4262  inrab  4263  inrab2  4264  difrab  4265  dfrab3ss  4270  rabun2  4271  dfnul2  4283  difid  4323  rabxm  4337  elnelun  4340  abf  4353  difdifdir  4439  dfif3  4487  dfif5  4489  rabsnif  4673  tpidm  4708  ssunpr  4783  sstp  4785  opidg  4841  dfint2  4897  iunrab  4999  uniiun  5005  intiin  5006  iunid  5007  0iin  5010  mptv  5195  dfepfr  5598  epfrc  5599  xpundi  5683  xpundir  5684  csbcnv  5822  resiun2  5948  resopab  5982  mptresid  5999  dffr3  6047  dfse2  6048  cnvun  6089  imaundir  6097  imainrect  6128  cnvcnv2  6140  cnvrescnv  6142  cnvcnvres  6152  dmtpop  6165  rnsnopg  6168  resdifdi  6183  rnco2  6201  dmco  6202  co01  6209  unidmrn  6226  dfdm2  6228  predidm  6273  dfmpt3  6615  mptun  6627  funcocnv2  6788  dffv2  6917  fnasrn  7078  fpr  7087  fmptap  7104  rnmptc  7141  riotav  7308  dmoprab  7449  rnoprab2  7452  mpov  7458  mpomptx  7459  abrexex2g  7896  1stval2  7938  2ndval2  7939  fo1st  7941  fo2nd  7942  xp2  7958  dfoprab4f  7988  offval22  8018  fmpoco  8025  fimaproj  8065  tposmpo  8193  tposconst  8194  recsfval  8300  rdgsucmpt2  8349  frsucmpt2  8359  df2o3  8393  o1p1e2  8455  o2p2e4  8456  oarec  8477  omopthlem2  8575  ecqs  8703  qliftf  8729  erovlem  8737  fset0  8778  mapsnf1o3  8819  ixp0x  8850  omf1o  8993  xpf1o  9052  mapunen  9059  enp1ilem  9162  marypha1lem  9317  marypha2lem4  9322  dfoi  9397  infeq5i  9526  oemapso  9572  cantnflem1  9579  rankelop  9767  leweon  9902  r0weon  9903  kmlem11  10052  dju1dif  10064  ackbij1lem16  10125  cf0  10142  cfsmolem  10161  alephsuc3  10471  fpwwe  10537  canthp1lem1  10543  wuncval2  10638  prlem936  10938  m1p1sr  10983  m1m1sr  10984  dfcnqs  11033  ssxr  11182  mul02lem2  11290  addrid  11293  2p2e4  12255  3p2e5  12271  3p3e6  12272  4p2e6  12273  4p3e7  12274  4p4e8  12275  5p2e7  12276  5p3e8  12277  5p4e9  12278  6p2e8  12279  6p3e9  12280  7p2e9  12281  nnzrab  12500  nn0zrab  12501  dec0u  12609  dec0h  12610  decsuc  12619  decsucc  12629  numma  12632  decma  12639  decmac  12640  decma2c  12641  decadd  12642  decaddc  12643  decmul1c  12653  decmul2c  12654  5p5e10  12659  6p4e10  12660  7p3e10  12663  8p2e10  12668  5t5e25  12691  6t6e36  12696  8t6e48  12707  nn0uz  12774  nnuz  12775  xaddcom  13139  x2times  13198  ioomax  13322  iccmax  13323  ioopos  13324  ioorp  13325  prunioo  13381  fseq1p1m1  13498  fzo13pr  13649  fzo0to2pr  13650  fzo0to3tp  13652  om2uzrdg  13863  fzennn  13875  irec  14108  sq10e99m1  14172  facnn  14182  fac0  14183  faclbnd2  14198  faclbnd4lem1  14200  hashfun  14344  hashbclem  14359  hashf1lem1  14362  hashf1lem2  14363  fz1isolem  14368  swrdccatin1  14632  swrdccat3blem  14646  s1co  14740  s2eq2s1eq  14843  s3eqs2s1eq  14845  ofs2  14878  dfid5  14934  dfid6  14935  fsumrev2  15689  fsumparts  15713  fsumiun  15728  isumnn0nn  15749  harmonic  15766  fprod2d  15888  bpoly2  15964  bpoly3  15965  bpoly4  15966  ege2le3  15997  cos1bnd  16096  efieq1re  16108  eirrlem  16113  qnnen  16122  cpnnen  16138  ruclem6  16144  3dvds  16242  pwp1fsum  16302  m1bits  16351  nn0expgcd  16475  algrp1  16485  phiprmpw  16687  prmreclem4  16831  4sqlem11  16867  4sqlem19  16875  dec5dvds  16976  decsplit1  16993  5prm  17020  7prm  17022  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  strle1  17069  grpbasex  17196  grpplusgx  17197  quslem  17447  xpsrnbas  17475  acsfn1  17567  acsfn2  17569  comfffval2  17607  dfinito2  17910  dftermo2  17911  xpchomfval  18085  xpccofval  18088  1stfval  18097  2ndfval  18100  oduleg  18196  chnub  18528  ismgmid  18573  efmndbas  18779  smndex2dnrinv  18823  grpinvfvi  18895  gaorb  19219  elcntr  19242  cntri  19244  cntrsubgnsg  19255  cntrnsg  19256  setsplusg  19262  oppgcntr  19277  gsumwrev  19278  symgressbas  19294  symgplusg  19295  symgvalstruct  19309  symgga  19319  cayleylem1  19324  psgnunilem2  19407  efgval2  19636  efgredlemc  19657  efgcpbllema  19666  frgpnabllem1  19785  gsumzaddlem  19833  gsumle  20057  opprlem  20260  oppr0  20267  opprneg  20269  rmodislmod  20863  rlmscaf  21141  xrsds  21346  gsumfsum  21371  zringunit  21403  pzriprng1  21435  cnmsgngrp  21516  psgnfix2  21536  relt  21552  ocv0  21614  thlle  21634  thlleval  21635  dsmmval2  21673  frlmip  21715  mplbas  21927  mplplusg  21944  mplmulr  21945  mplvsca2  21951  ressmplbas2  21962  ltbwe  21979  evlslem4  22011  psdmul  22081  psr1bas2  22102  ply1bas  22107  ply1basOLD  22108  ply1assa  22112  psr1plusg  22133  psr1vsca  22134  psr1mulr  22135  ply1plusg  22136  ply1vsca  22137  ply1mulr  22138  ply1mpl0  22169  ply1mpl1  22171  coe1mul  22184  matgsum  22352  smadiadetglem1  22586  indistpsx  22925  iuncld  22960  tgrest  23074  resstopn  23101  leordtval2  23127  xkouni  23514  ptclsg  23530  ptuncnv  23722  ptunhmeo  23723  alexsubALTlem4  23965  tsmsf1o  24060  ucnimalem  24194  ressxms  24440  uniretop  24677  cnfldtopn  24696  xrtgioo  24722  zcld  24729  icccmp  24741  xrge0gsumle  24749  xrge0tsms  24750  metnrmlem3  24777  fsum2cn  24789  cnmpopc  24849  oprpiece1res1  24876  oprpiece1res2  24877  evth  24885  evth2  24886  om1opn  24963  pi1xfrf  24980  pi1xfrcnv  24984  pi1cof  24986  clsocv  25177  cncmet  25249  cnflduss  25283  rrxprds  25316  ehlbase  25342  ismbl  25454  shftmbl  25466  ioorinv  25504  itg1addlem4  25627  itg2cnlem1  25689  itg0  25708  itgss3  25743  ditgneg  25785  limcdif  25804  limciun  25822  dvexp  25884  dvef  25911  dvcnvrelem2  25950  ftc1  25976  aannenlem2  26264  dvradcnv  26357  pserdvlem2  26365  reefgim  26387  cospi  26408  sincos6thpi  26452  tanregt0  26475  dflog2  26496  logfac  26537  dvlog  26587  cxpexp  26604  cxpmul2  26625  cxpsqrt  26639  dvsqrt  26678  dvcnsqrt  26680  cxpcn2  26683  isosctrlem2  26756  1cubrlem  26778  1cubr  26779  quart1lem  26792  atancj  26847  atanlogaddlem  26850  atansopn  26869  leibpilem2  26878  log2cnv  26881  log2ublem3  26885  birthdaylem1  26888  birthdaylem2  26889  birthday  26891  dfarea  26897  lgamgulmlem5  26970  lgambdd  26974  ftalem3  27012  basellem2  27019  ppiprm  27088  ppinprm  27089  chtprm  27090  chtnprm  27091  ppi2  27107  ppi3  27108  ppiub  27142  chtub  27150  bclbnd  27218  bposlem8  27229  lgsdilem  27262  lgsdir2lem2  27264  lgsquadlem2  27319  lgsquad2lem2  27323  2lgsoddprmlem3c  27350  rplogsum  27465  mulog2sumlem2  27473  pnt2  27551  bdayfo  27616  bday0s  27772  bday1s  27775  old1  27820  addsasslem2  27947  negsbdaylem  27998  muls01  28051  abssnid  28181  1p1e2s  28339  n0seo  28344  twocut  28346  halfcut  28378  pw2cutp1  28381  pw2cut2  28382  zs12bday  28394  istrkg2ld  28438  axsegconlem9  28903  ax5seglem7  28913  iedgedg  29028  uspgrf1oedg  29151  nbgrcl  29313  nbgrnvtx0  29317  rusgrprc  29569  pthsfval  29697  wlkiswwlks2lem4  29850  wlkiswwlks2lem5  29851  clwwlkvbij  30093  konigsbergumgr  30231  ex-pw  30409  ex-xp  30416  ex-rn  30420  nvvop  30589  nvm  30621  cnims  30673  ip0i  30805  ip1ilem  30806  ipdirilem  30809  ipasslem10  30819  h2hva  30954  h2hsm  30955  h2hvs  30957  axhfvadd-zf  30962  axhvcom-zf  30963  axhvass-zf  30964  axhv0cl-zf  30965  axhvaddid-zf  30966  axhfvmul-zf  30967  axhvmulid-zf  30968  axhvmulass-zf  30969  axhvdistr1-zf  30970  axhvdistr2-zf  30971  axhvmul0-zf  30972  axhfi-zf  30973  axhis1-zf  30974  axhis2-zf  30975  axhis3-zf  30976  axhis4-zf  30977  axhcompl-zf  30978  normlem0  31089  normlem1  31090  normlem2  31091  normlem4  31093  normlem9  31098  bcseqi  31100  dfhnorm2  31102  norm3difi  31127  normpari  31134  normpar2i  31136  polid2i  31137  polidi  31138  hhba  31147  hhims  31152  hhims2  31153  hhsssh  31249  hhssims  31254  hhssims2  31255  shsval3i  31368  dfch2  31387  cmcm2i  31573  fh2  31599  qlaxr3i  31616  spansnji  31626  pjcji  31664  ho0val  31730  df0op2  31732  hosd1i  31802  hosd2i  31803  eigorthi  31817  hhlnoi  31880  hhnmoi  31881  hhbloi  31882  bra0  31930  nmop0  31966  nmfn0  31967  lnopeq0lem1  31985  lnopunilem1  31990  lnophmlem2  31997  nmopcoadji  32081  pjhmopidm  32163  cvmdi  32304  cdj3lem3  32418  cdj3lem3b  32420  abrexdomjm  32487  uniin1  32531  uniin2  32532  iundifdifd  32541  iundifdif  32542  mpomptxf  32659  df1stres  32685  df2ndres  32686  intimafv  32692  fcobijfs  32704  fcobijfs2  32705  resf1o  32713  fpwrelmapffslem  32715  sgnneg  32816  dpval3  32874  dp3mul10  32878  dpadd2  32890  dpmul4  32894  ccatws1f1o  32932  xrslt  32988  xrsclat  32992  xrge0tsmsd  33042  cycpmco2lem7  33101  cycpmconjv  33111  cycpmrn  33112  conjga  33139  elrgspnsubrunlem2  33215  rndrhmcl  33262  fracf1  33273  xrge0slmod  33313  lsmsnorb2  33357  qusbas2  33371  1arithidomlem2  33501  zringfrac  33519  mplvrpmga  33575  mplvrpmmhm  33576  mplvrpmrhm  33577  rlmdim  33622  rgmoddimOLD  33623  isconstr  33749  iconstr  33779  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  circtopn  33850  tpr2rico  33925  xrge0mulc1cn  33954  lmxrge0  33965  esumpfinvallem  34087  esumcocn  34093  hasheuni  34098  esumcvg  34099  rossros  34193  measinblem  34233  aean  34257  sxbrsigalem3  34285  dya2iocival  34286  dya2iocucvr  34297  sxbrsigalem1  34298  sxbrsigalem2  34299  sxbrsigalem5  34301  sxbrsiga  34303  fiunelcarsg  34329  eulerpartlem1  34380  eulerpartgbij  34385  fibp1  34414  coinfliplem  34492  coinflipprob  34493  ballotlemfval  34503  ballotth  34551  plymulx  34561  circlemethhgt  34656  hgt750lem2  34665  bnj1400  34847  bnj66  34872  bnj882  34938  lfuhgr  35162  derang0  35213  subfacp1lem1  35223  subfacp1lem6  35229  kur14lem7  35256  cvmsss2  35318  cvmliftlem8  35336  cvmliftlem10  35338  satfv1lem  35406  msubfval  35568  quad3  35714  bcprod  35782  bccolsum  35783  faclim  35790  pprodcnveq  35925  dfon4  35935  fobigcup  35942  dfiota3  35965  dfrecs2  35994  dfrdg4  35995  dfint3  35996  rankeq1o  36215  refssfne  36402  ssoninhaus  36492  onint1  36493  bj-rababw  36925  bj-inrab3  36973  bj-imdiridlem  37229  dissneq  37385  dffinxpf  37429  finxpreclem4  37438  rabiun  37632  ptrest  37658  poimirlem3  37662  poimirlem4  37663  poimirlem13  37672  poimirlem16  37675  poimirlem22  37681  poimirlem26  37685  poimirlem27  37686  poimirlem30  37689  cnambfre  37707  ftc1anclem8  37739  fnopabco  37762  abrexdom  37769  cncfres  37804  scottexf  38207  scott0f  38208  inres2  38281  dfres4  38330  dmxrn  38410  xrnres  38448  xrnres2  38449  dfsucmap2  38476  dfcoss2  38514  dfcoss4  38516  1cossres  38530  dmcoss2  38555  1cosscnvxrn  38576  dfeqvrels2  38683  dfcoeleqvrels  38716  redundss3  38723  dffunsALTV5  38784  cdleme3d  40329  cdleme7a  40341  cdleme31sdnN  40485  cdlemk45  41045  420gcd8e4  42098  lcmeprodgcdi  42099  60lcm7e420  42102  420lcm8e840  42103  3lexlogpow5ineq1  42146  3lexlogpow2ineq1  42150  3lexlogpow2ineq2  42151  3lexlogpow5ineq5  42152  aks4d1p1  42168  posbezout  42192  aks6d1c1p4  42203  aks6d1c3  42215  2ap1caineq  42237  sticksstones7  42244  sticksstones12a  42249  sticksstones12  42250  aks6d1c6lem4  42265  imaopab  42323  fmpocos  42326  dfqs2  42329  dfqs3  42330  decaddcom  42376  sumcubes  42405  redvmptabs  42452  readvrec  42454  readvcot  42456  sn-00idlem2  42491  reixi  42515  sum9cubes  42764  mapfzcons  42808  eldioph4b  42903  diophren  42905  pwssplit4  43181  pwfi2f1o  43188  frlmpwfi  43190  mendplusgfval  43273  mendmulrfval  43275  mendvscafval  43278  idomodle  43283  cytpval  43294  arearect  43307  onov0suclim  43366  omabs2  43424  tr3dom  43620  har2o  43638  alephiso2  43650  alephiso3  43651  relintab  43675  dfid7  43704  cnvrcl0  43717  dfrtrcl5  43721  dfrcl3  43767  dfrcl4  43768  comptiunov2i  43798  corcltrcl  43831  neicvgnvo  44207  inductionexd  44247  mnuprdlem2  44365  nznngen  44408  hashnzfz2  44413  lhe4.4ex1a  44421  dvradcnv2  44439  binomcxplemrat  44442  binomcxplemnotnn0  44448  nregmodelf1o  45107  refsum2cnlem1  45133  fiiuncl  45161  iccdifprioo  45615  lptre2pt  45737  limclner  45748  stoweidlem13  46110  stoweidlem32  46129  stoweidlem62  46159  wallispi2lem2  46169  stirlinglem14  46184  dirkertrigeqlem1  46195  dirkercncflem4  46203  fourierdlem42  46246  fourierdlem73  46276  fourierdlem81  46284  fourierdlem92  46295  fourierdlem103  46306  fourierdlem104  46307  fouriercnp  46323  fouriersw  46328  sge0tsms  46477  sge0iunmptlemfi  46510  ovolval5lem3  46751  cnfsmf  46837  nthrucw  46983  lamberte  46987  rnfdmpr  47380  fvmptrabdm  47392  fundcmpsurinjlem1  47497  m11nprm  47700  opoeALTV  47782  nfermltl8rev  47841  sbgoldbo  47886  evengpop3  47897  clnbgrcl  47920  clnbgrnvtx0  47926  usgrexmpl2edg  48128  usgrexmpl2nb0  48130  usgrexmpl2nb3  48133  gpg5order  48159  gpgprismgr4cycllem6  48199  cznabel  48359  cznrng  48360  mpomptx2  48434  2sphere  48849  itscnhlinecirc02plem3  48884  inlinecirc02p  48887  dftpos5  48973  tposresg  48977  icccldii  49018  dfnrm2  49031  dfnrm3  49032  elxpcbasex1ALT  49349  elxpcbasex2ALT  49351  dfswapf2  49361  swapf1a  49369  swapf1f1o  49375  swapf2f1oa  49377  swapfida  49380  setc1oterm  49591  setc1ohomfval  49593  setc1ocofval  49594  funcsetc1o  49597  dfinito4  49601  setc1onsubc  49702  islmd  49765  iscmd  49766  initocmd  49769  termolmd  49770  amgmlemALT  49903