Theorem eqtr4i 2763

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 2746	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2760	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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtr2i  2766  3eqtr2ri  2767  3eqtr4i  2770  3eqtr4ri  2771  rabab  3461  cbvralcsf  3880  cbvrabcsf  3883  dfin5  3898  dfdif2  3899  uneqin  4230  notabw  4254  unrab  4256  inrab  4257  inrab2  4258  difrab  4259  dfrab3ss  4264  rabun2  4265  dfnul2  4277  difid  4317  rabxm  4331  elnelun  4334  abf  4347  difdifdir  4432  dfif3  4482  dfif5  4484  rabsnif  4668  tpidm  4703  ssunpr  4778  sstp  4780  opidg  4836  dfint2  4892  iunrab  4996  uniiun  5002  intiin  5003  iunid  5004  0iin  5007  mptv  5192  dfepfr  5609  epfrc  5610  xpundi  5694  xpundir  5695  csbcnv  5833  resiun2  5960  resopab  5994  mptresid  6011  dffr3  6059  dfse2  6060  cnvun  6101  imaundir  6109  imainrect  6140  cnvcnv2  6152  cnvrescnv  6154  cnvcnvres  6164  dmtpop  6177  rnsnopg  6180  resdifdi  6195  rnco2  6213  dmco  6214  co01  6221  unidmrn  6238  dfdm2  6240  predidm  6285  dfmpt3  6627  mptun  6639  funcocnv2  6800  dffv2  6930  fnasrn  7093  fpr  7102  fmptap  7119  rnmptc  7156  riotav  7323  dmoprab  7464  rnoprab2  7467  mpov  7473  mpomptx  7474  abrexex2g  7911  1stval2  7953  2ndval2  7954  fo1st  7956  fo2nd  7957  xp2  7973  dfoprab4f  8003  offval22  8032  fmpoco  8039  fimaproj  8079  tposmpo  8207  tposconst  8208  recsfval  8314  rdgsucmpt2  8363  frsucmpt2  8373  df2o3  8407  o1p1e2  8469  o2p2e4  8470  oarec  8491  omopthlem2  8590  dfqs2  8644  ecqs  8720  qliftf  8746  erovlem  8754  fset0  8795  mapsnf1o3  8837  ixp0x  8868  omf1o  9012  xpf1o  9071  mapunen  9078  enp1ilem  9182  marypha1lem  9340  marypha2lem4  9345  dfoi  9420  infeq5i  9551  oemapso  9597  cantnflem1  9604  rankelop  9792  leweon  9927  r0weon  9928  kmlem11  10077  dju1dif  10089  ackbij1lem16  10150  cf0  10167  cfsmolem  10186  alephsuc3  10497  fpwwe  10563  canthp1lem1  10569  wuncval2  10664  prlem936  10964  m1p1sr  11009  m1m1sr  11010  dfcnqs  11059  ssxr  11209  mul02lem2  11317  addrid  11320  2p2e4  12305  3p2e5  12321  3p3e6  12322  4p2e6  12323  4p3e7  12324  4p4e8  12325  5p2e7  12326  5p3e8  12327  5p4e9  12328  6p2e8  12329  6p3e9  12330  7p2e9  12331  nnzrab  12549  nn0zrab  12550  dec0u  12659  dec0h  12660  decsuc  12669  decsucc  12679  numma  12682  decma  12689  decmac  12690  decma2c  12691  decadd  12692  decaddc  12693  decmul1c  12703  decmul2c  12704  5p5e10  12709  6p4e10  12710  7p3e10  12713  8p2e10  12718  5t5e25  12741  6t6e36  12746  8t6e48  12757  nn0uz  12820  nnuz  12821  xaddcom  13186  x2times  13245  ioomax  13369  iccmax  13370  ioopos  13371  ioorp  13372  prunioo  13428  fseq1p1m1  13546  fzo13pr  13698  fzo0to2pr  13699  fzo0to3tp  13701  om2uzrdg  13912  fzennn  13924  irec  14157  sq10e99m1  14221  facnn  14231  fac0  14232  faclbnd2  14247  faclbnd4lem1  14249  hashfun  14393  hashbclem  14408  hashf1lem1  14411  hashf1lem2  14412  fz1isolem  14417  swrdccatin1  14681  swrdccat3blem  14695  s1co  14789  s2eq2s1eq  14892  s3eqs2s1eq  14894  ofs2  14927  dfid5  14983  dfid6  14984  fsumrev2  15738  fsumparts  15763  fsumiun  15778  isumnn0nn  15801  harmonic  15818  fprod2d  15940  bpoly2  16016  bpoly3  16017  bpoly4  16018  ege2le3  16049  cos1bnd  16148  efieq1re  16160  eirrlem  16165  qnnen  16174  cpnnen  16190  ruclem6  16196  3dvds  16294  pwp1fsum  16354  m1bits  16403  nn0expgcd  16527  algrp1  16537  phiprmpw  16740  prmreclem4  16884  4sqlem11  16920  4sqlem19  16928  dec5dvds  17029  decsplit1  17046  5prm  17073  7prm  17075  1259lem2  17096  1259lem3  17097  1259lem4  17098  1259lem5  17099  1259prm  17100  2503lem1  17101  2503lem2  17102  2503lem3  17103  2503prm  17104  4001lem1  17105  4001lem2  17106  4001lem3  17107  4001lem4  17108  4001prm  17109  strle1  17122  grpbasex  17249  grpplusgx  17250  quslem  17501  xpsrnbas  17529  acsfn1  17621  acsfn2  17623  comfffval2  17661  dfinito2  17964  dftermo2  17965  xpchomfval  18139  xpccofval  18142  1stfval  18151  2ndfval  18154  oduleg  18250  chnub  18582  ismgmid  18627  efmndbas  18833  smndex2dnrinv  18880  grpinvfvi  18952  gaorb  19276  elcntr  19299  cntri  19301  cntrsubgnsg  19312  cntrnsg  19313  setsplusg  19319  oppgcntr  19334  gsumwrev  19335  symgressbas  19351  symgplusg  19352  symgvalstruct  19366  symgga  19376  cayleylem1  19381  psgnunilem2  19464  efgval2  19693  efgredlemc  19714  efgcpbllema  19723  frgpnabllem1  19842  gsumzaddlem  19890  gsumle  20114  opprlem  20316  oppr0  20323  opprneg  20325  rmodislmod  20919  rlmscaf  21197  xrsds  21402  gsumfsum  21427  zringunit  21459  pzriprng1  21491  cnmsgngrp  21572  psgnfix2  21592  relt  21608  ocv0  21670  thlle  21690  thlleval  21691  dsmmval2  21729  frlmip  21771  mplbas  21981  mplplusg  21998  mplmulr  21999  mplvsca2  22005  ressmplbas2  22018  ltbwe  22035  evlslem4  22067  psdmul  22145  psr1bas2  22166  ply1bas  22171  ply1basOLD  22172  ply1assa  22176  psr1plusg  22197  psr1vsca  22198  psr1mulr  22199  ply1plusg  22200  ply1vsca  22201  ply1mulr  22202  ply1mpl0  22233  ply1mpl1  22235  coe1mul  22248  matgsum  22415  smadiadetglem1  22649  indistpsx  22988  iuncld  23023  tgrest  23137  resstopn  23164  leordtval2  23190  xkouni  23577  ptclsg  23593  ptuncnv  23785  ptunhmeo  23786  alexsubALTlem4  24028  tsmsf1o  24123  ucnimalem  24257  ressxms  24503  uniretop  24740  cnfldtopn  24759  xrtgioo  24785  zcld  24792  icccmp  24804  xrge0gsumle  24812  xrge0tsms  24813  metnrmlem3  24840  fsum2cn  24851  cnmpopc  24908  oprpiece1res1  24931  oprpiece1res2  24932  evth  24939  evth2  24940  om1opn  25016  pi1xfrf  25033  pi1xfrcnv  25037  pi1cof  25039  clsocv  25230  cncmet  25302  cnflduss  25336  rrxprds  25369  ehlbase  25395  ismbl  25506  shftmbl  25518  ioorinv  25556  itg1addlem4  25679  itg2cnlem1  25741  itg0  25760  itgss3  25795  ditgneg  25837  limcdif  25856  limciun  25874  dvexp  25933  dvef  25960  dvcnvrelem2  25998  ftc1  26022  aannenlem2  26309  dvradcnv  26402  pserdvlem2  26409  reefgim  26431  cospi  26452  sincos6thpi  26496  tanregt0  26519  dflog2  26540  logfac  26581  dvlog  26631  cxpexp  26648  cxpmul2  26669  cxpsqrt  26683  dvsqrt  26722  dvcnsqrt  26724  cxpcn2  26726  isosctrlem2  26799  1cubrlem  26821  1cubr  26822  quart1lem  26835  atancj  26890  atanlogaddlem  26893  atansopn  26912  leibpilem2  26921  log2cnv  26924  log2ublem3  26928  birthdaylem1  26931  birthdaylem2  26932  birthday  26934  dfarea  26940  lgamgulmlem5  27013  lgambdd  27017  ftalem3  27055  basellem2  27062  ppiprm  27131  ppinprm  27132  chtprm  27133  chtnprm  27134  ppi2  27150  ppi3  27151  ppiub  27184  chtub  27192  bclbnd  27260  bposlem8  27271  lgsdilem  27304  lgsdir2lem2  27306  lgsquadlem2  27361  lgsquad2lem2  27365  2lgsoddprmlem3c  27392  rplogsum  27507  mulog2sumlem2  27515  pnt2  27593  bdayfo  27658  bday0  27820  bday1  27823  old1  27874  addsasslem2  28013  negbdaylem  28065  muls01  28121  abssnid  28252  1p1e2s  28425  n0seo  28430  twocut  28432  halfcut  28467  pw2cutp1  28470  pw2cut2  28471  istrkg2ld  28545  axsegconlem9  29011  ax5seglem7  29021  iedgedg  29136  uspgrf1oedg  29259  nbgrcl  29421  nbgrnvtx0  29425  rusgrprc  29677  pthsfval  29805  wlkiswwlks2lem4  29958  wlkiswwlks2lem5  29959  clwwlkvbij  30201  konigsbergumgr  30339  ex-pw  30517  ex-xp  30524  ex-rn  30528  nvvop  30698  nvm  30730  cnims  30782  ip0i  30914  ip1ilem  30915  ipdirilem  30918  ipasslem10  30928  h2hva  31063  h2hsm  31064  h2hvs  31066  axhfvadd-zf  31071  axhvcom-zf  31072  axhvass-zf  31073  axhv0cl-zf  31074  axhvaddid-zf  31075  axhfvmul-zf  31076  axhvmulid-zf  31077  axhvmulass-zf  31078  axhvdistr1-zf  31079  axhvdistr2-zf  31080  axhvmul0-zf  31081  axhfi-zf  31082  axhis1-zf  31083  axhis2-zf  31084  axhis3-zf  31085  axhis4-zf  31086  axhcompl-zf  31087  normlem0  31198  normlem1  31199  normlem2  31200  normlem4  31202  normlem9  31207  bcseqi  31209  dfhnorm2  31211  norm3difi  31236  normpari  31243  normpar2i  31245  polid2i  31246  polidi  31247  hhba  31256  hhims  31261  hhims2  31262  hhsssh  31358  hhssims  31363  hhssims2  31364  shsval3i  31477  dfch2  31496  cmcm2i  31682  fh2  31708  qlaxr3i  31725  spansnji  31735  pjcji  31773  ho0val  31839  df0op2  31841  hosd1i  31911  hosd2i  31912  eigorthi  31926  hhlnoi  31989  hhnmoi  31990  hhbloi  31991  bra0  32039  nmop0  32075  nmfn0  32076  lnopeq0lem1  32094  lnopunilem1  32099  lnophmlem2  32106  nmopcoadji  32190  pjhmopidm  32272  cvmdi  32413  cdj3lem3  32527  cdj3lem3b  32529  abrexdomjm  32595  uniin1  32639  uniin2  32640  iundifdifd  32649  iundifdif  32650  mpomptxf  32769  df1stres  32795  df2ndres  32796  intimafv  32802  fcobijfs  32812  fcobijfs2  32813  resf1o  32821  fpwrelmapffslem  32823  sgnneg  32924  dpval3  32971  dp3mul10  32975  dpadd2  32987  dpmul4  32991  ccatws1f1o  33029  xrslt  33085  xrsclat  33089  xrge0tsmsd  33152  cycpmco2lem7  33211  cycpmconjv  33221  cycpmrn  33222  conjga  33249  elrgspnsubrunlem2  33327  rndrhmcl  33375  fracf1  33386  xrge0slmod  33426  lsmsnorb2  33470  qusbas2  33484  1arithidomlem2  33614  zringfrac  33632  mplvrpmga  33707  mplvrpmmhm  33708  mplvrpmrhm  33709  psrmonprod  33714  mplmonprod  33716  vieta  33742  rlmdim  33772  rgmoddimOLD  33773  isconstr  33899  iconstr  33929  cos9thpiminplylem4  33948  cos9thpiminplylem5  33949  circtopn  34000  tpr2rico  34075  xrge0mulc1cn  34104  lmxrge0  34115  esumpfinvallem  34237  esumcocn  34243  hasheuni  34248  esumcvg  34249  rossros  34343  measinblem  34383  aean  34407  sxbrsigalem3  34435  dya2iocival  34436  dya2iocucvr  34447  sxbrsigalem1  34448  sxbrsigalem2  34449  sxbrsigalem5  34451  sxbrsiga  34453  fiunelcarsg  34479  eulerpartlem1  34530  eulerpartgbij  34535  fibp1  34564  coinfliplem  34642  coinflipprob  34643  ballotlemfval  34653  ballotth  34701  plymulx  34711  circlemethhgt  34806  hgt750lem2  34815  bnj1400  34996  bnj66  35021  bnj882  35087  lfuhgr  35319  derang0  35370  subfacp1lem1  35380  subfacp1lem6  35386  kur14lem7  35413  cvmsss2  35475  cvmliftlem8  35493  cvmliftlem10  35495  satfv1lem  35563  msubfval  35725  quad3  35871  bcprod  35939  bccolsum  35940  faclim  35947  pprodcnveq  36082  dfon4  36092  fobigcup  36099  dfiota3  36122  dfrecs2  36151  dfrdg4  36152  dfint3  36153  rankeq1o  36372  refssfne  36559  ssoninhaus  36649  onint1  36650  ttciun  36715  bj-dfnul2  36854  bj-rababw  37207  bj-inrab3  37255  bj-imdiridlem  37518  dissneq  37674  dffinxpf  37718  finxpreclem4  37727  rabiun  37931  ptrest  37957  poimirlem3  37961  poimirlem4  37962  poimirlem13  37971  poimirlem16  37974  poimirlem22  37980  poimirlem26  37984  poimirlem27  37985  poimirlem30  37988  cnambfre  38006  ftc1anclem8  38038  fnopabco  38061  abrexdom  38068  cncfres  38103  scottexf  38506  scott0f  38507  inres2  38585  eqrabi  38594  xpv  38600  dfres4  38637  dmxrn  38725  xrnres  38763  xrnres2  38764  rnqmap  38792  dfsucmap2  38802  dfcoss2  38841  dfcoss4  38843  1cossres  38857  dmcoss2  38882  1cosscnvxrn  38903  dfeqvrels2  39010  dfcoeleqvrels  39043  redundss3  39050  dffunsALTV5  39110  dfpeters2  39312  cdleme3d  40694  cdleme7a  40706  cdleme31sdnN  40850  cdlemk45  41410  420gcd8e4  42462  lcmeprodgcdi  42463  60lcm7e420  42466  420lcm8e840  42467  3lexlogpow5ineq1  42510  3lexlogpow2ineq1  42514  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  aks4d1p1  42532  posbezout  42556  aks6d1c1p4  42567  aks6d1c3  42579  2ap1caineq  42601  sticksstones7  42608  sticksstones12a  42613  sticksstones12  42614  aks6d1c6lem4  42629  imaopab  42689  fmpocos  42692  dfqs3  42695  decaddcom  42733  sumcubes  42762  redvmptabs  42809  readvrec  42811  readvcot  42813  sn-00idlem2  42848  reixi  42872  sum9cubes  43122  mapfzcons  43165  eldioph4b  43260  diophren  43262  pwssplit4  43538  pwfi2f1o  43545  frlmpwfi  43547  mendplusgfval  43630  mendmulrfval  43632  mendvscafval  43635  idomodle  43640  cytpval  43651  arearect  43664  onov0suclim  43723  omabs2  43781  tr3dom  43976  har2o  43994  alephiso2  44006  alephiso3  44007  relintab  44031  dfid7  44060  cnvrcl0  44073  dfrtrcl5  44077  dfrcl3  44123  dfrcl4  44124  comptiunov2i  44154  corcltrcl  44187  neicvgnvo  44563  inductionexd  44603  mnuprdlem2  44721  nznngen  44764  hashnzfz2  44769  lhe4.4ex1a  44777  dvradcnv2  44795  binomcxplemrat  44798  binomcxplemnotnn0  44804  nregmodelf1o  45463  refsum2cnlem1  45489  fiiuncl  45517  iccdifprioo  45967  lptre2pt  46089  limclner  46100  stoweidlem13  46462  stoweidlem32  46481  stoweidlem62  46511  wallispi2lem2  46521  stirlinglem14  46536  dirkertrigeqlem1  46547  dirkercncflem4  46555  fourierdlem42  46598  fourierdlem73  46628  fourierdlem81  46636  fourierdlem92  46647  fourierdlem103  46658  fourierdlem104  46659  fouriercnp  46675  fouriersw  46680  sge0tsms  46829  sge0iunmptlemfi  46862  ovolval5lem3  47103  cnfsmf  47189  nthrucw  47335  lamberte  47351  rnfdmpr  47744  fvmptrabdm  47756  fundcmpsurinjlem1  47873  m11nprm  48079  ppi1sum  48109  opoeALTV  48174  nfermltl8rev  48233  sbgoldbo  48278  evengpop3  48289  clnbgrcl  48312  clnbgrnvtx0  48318  usgrexmpl2edg  48520  usgrexmpl2nb0  48522  usgrexmpl2nb3  48525  gpg5order  48551  gpgprismgr4cycllem6  48591  cznabel  48751  cznrng  48752  mpomptx2  48826  2sphere  49240  itscnhlinecirc02plem3  49275  inlinecirc02p  49278  dftpos5  49364  tposresg  49368  icccldii  49409  dfnrm2  49422  dfnrm3  49423  elxpcbasex1ALT  49739  elxpcbasex2ALT  49741  dfswapf2  49751  swapf1a  49759  swapf1f1o  49765  swapf2f1oa  49767  swapfida  49770  setc1oterm  49981  setc1ohomfval  49983  setc1ocofval  49984  funcsetc1o  49987  dfinito4  49991  setc1onsubc  50092  islmd  50155  iscmd  50156  initocmd  50159  termolmd  50160  amgmlemALT  50293