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  3467  cbvralcsf  3893  cbvrabcsf  3896  dfin5  3911  dfdif2  3912  uneqin  4240  notabw  4264  unrab  4266  inrab  4267  inrab2  4268  difrab  4269  dfrab3ss  4274  rabun2  4275  dfnul2  4287  difid  4327  rabxm  4341  elnelun  4344  abf  4357  difdifdir  4443  dfif3  4491  dfif5  4493  rabsnif  4675  tpidm  4710  ssunpr  4785  sstp  4787  opidg  4843  dfint2  4898  iunrab  5001  uniiun  5007  intiin  5008  iunid  5009  0iin  5013  mptv  5198  dfepfr  5603  epfrc  5604  xpundi  5688  xpundir  5689  csbcnv  5826  resiun2  5951  resopab  5985  mptresid  6002  dffr3  6050  dfse2  6051  cnvun  6091  imaundir  6099  imainrect  6130  cnvcnv2  6142  cnvrescnv  6144  cnvcnvres  6154  dmtpop  6167  rnsnopg  6170  resdifdi  6185  rnco2  6202  dmco  6203  co01  6210  unidmrn  6227  dfdm2  6229  predidm  6274  dfmpt3  6616  mptun  6628  funcocnv2  6789  dffv2  6918  fnasrn  7079  fpr  7088  fmptap  7106  rnmptc  7143  riotav  7311  dmoprab  7452  rnoprab2  7455  mpov  7461  mpomptx  7462  abrexex2g  7899  1stval2  7941  2ndval2  7942  fo1st  7944  fo2nd  7945  xp2  7961  dfoprab4f  7991  offval22  8021  fmpoco  8028  fimaproj  8068  tposmpo  8196  tposconst  8197  recsfval  8303  rdgsucmpt2  8352  frsucmpt2  8362  df2o3  8396  o1p1e2  8458  o2p2e4  8459  oarec  8480  omopthlem2  8578  ecqs  8706  qliftf  8732  erovlem  8740  fset0  8781  mapsnf1o3  8822  ixp0x  8853  omf1o  8997  xpf1o  9056  mapunen  9063  enp1ilem  9167  marypha1lem  9323  marypha2lem4  9328  dfoi  9403  infeq5i  9532  oemapso  9578  cantnflem1  9585  rankelop  9770  leweon  9905  r0weon  9906  kmlem11  10055  dju1dif  10067  ackbij1lem16  10128  cf0  10145  cfsmolem  10164  alephsuc3  10474  fpwwe  10540  canthp1lem1  10546  wuncval2  10641  prlem936  10941  m1p1sr  10986  m1m1sr  10987  dfcnqs  11036  ssxr  11185  mul02lem2  11293  addrid  11296  2p2e4  12258  3p2e5  12274  3p3e6  12275  4p2e6  12276  4p3e7  12277  4p4e8  12278  5p2e7  12279  5p3e8  12280  5p4e9  12281  6p2e8  12282  6p3e9  12283  7p2e9  12284  nnzrab  12503  nn0zrab  12504  dec0u  12612  dec0h  12613  decsuc  12622  decsucc  12632  numma  12635  decma  12642  decmac  12643  decma2c  12644  decadd  12645  decaddc  12646  decmul1c  12656  decmul2c  12657  5p5e10  12662  6p4e10  12663  7p3e10  12666  8p2e10  12671  5t5e25  12694  6t6e36  12699  8t6e48  12710  nn0uz  12777  nnuz  12778  xaddcom  13142  x2times  13201  ioomax  13325  iccmax  13326  ioopos  13327  ioorp  13328  prunioo  13384  fseq1p1m1  13501  fzo13pr  13652  fzo0to2pr  13653  fzo0to3tp  13655  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  14631  swrdccat3blem  14645  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  ismgmid  18539  efmndbas  18745  smndex2dnrinv  18789  grpinvfvi  18861  gaorb  19186  elcntr  19209  cntri  19211  cntrsubgnsg  19222  cntrnsg  19223  setsplusg  19229  oppgcntr  19244  gsumwrev  19245  symgressbas  19261  symgplusg  19262  symgvalstruct  19276  symgga  19286  cayleylem1  19291  psgnunilem2  19374  efgval2  19603  efgredlemc  19624  efgcpbllema  19633  frgpnabllem1  19752  gsumzaddlem  19800  gsumle  20024  opprlem  20227  oppr0  20234  opprneg  20236  rmodislmod  20833  rlmscaf  21111  xrsds  21316  gsumfsum  21341  zringunit  21373  pzriprng1  21405  cnmsgngrp  21486  psgnfix2  21506  relt  21522  ocv0  21584  thlle  21604  thlleval  21605  dsmmval2  21643  frlmip  21685  mplbas  21897  mplplusg  21914  mplmulr  21915  mplvsca2  21921  ressmplbas2  21932  ltbwe  21949  evlslem4  21981  psdmul  22051  psr1bas2  22072  ply1bas  22077  ply1basOLD  22078  ply1assa  22082  psr1plusg  22103  psr1vsca  22104  psr1mulr  22105  ply1plusg  22106  ply1vsca  22107  ply1mulr  22108  ply1mpl0  22139  ply1mpl1  22141  coe1mul  22154  matgsum  22322  smadiadetglem1  22556  indistpsx  22895  iuncld  22930  tgrest  23044  resstopn  23071  leordtval2  23097  xkouni  23484  ptclsg  23500  ptuncnv  23692  ptunhmeo  23693  alexsubALTlem4  23935  tsmsf1o  24030  ucnimalem  24165  ressxms  24411  uniretop  24648  cnfldtopn  24667  xrtgioo  24693  zcld  24700  icccmp  24712  xrge0gsumle  24720  xrge0tsms  24721  metnrmlem3  24748  fsum2cn  24760  cnmpopc  24820  oprpiece1res1  24847  oprpiece1res2  24848  evth  24856  evth2  24857  om1opn  24934  pi1xfrf  24951  pi1xfrcnv  24955  pi1cof  24957  clsocv  25148  cncmet  25220  cnflduss  25254  rrxprds  25287  ehlbase  25313  ismbl  25425  shftmbl  25437  ioorinv  25475  itg1addlem4  25598  itg2cnlem1  25660  itg0  25679  itgss3  25714  ditgneg  25756  limcdif  25775  limciun  25793  dvexp  25855  dvef  25882  dvcnvrelem2  25921  ftc1  25947  aannenlem2  26235  dvradcnv  26328  pserdvlem2  26336  reefgim  26358  cospi  26379  sincos6thpi  26423  tanregt0  26446  dflog2  26467  logfac  26508  dvlog  26558  cxpexp  26575  cxpmul2  26596  cxpsqrt  26610  dvsqrt  26649  dvcnsqrt  26651  cxpcn2  26654  isosctrlem2  26727  1cubrlem  26749  1cubr  26750  quart1lem  26763  atancj  26818  atanlogaddlem  26821  atansopn  26840  leibpilem2  26849  log2cnv  26852  log2ublem3  26856  birthdaylem1  26859  birthdaylem2  26860  birthday  26862  dfarea  26868  lgamgulmlem5  26941  lgambdd  26945  ftalem3  26983  basellem2  26990  ppiprm  27059  ppinprm  27060  chtprm  27061  chtnprm  27062  ppi2  27078  ppi3  27079  ppiub  27113  chtub  27121  bclbnd  27189  bposlem8  27200  lgsdilem  27233  lgsdir2lem2  27235  lgsquadlem2  27290  lgsquad2lem2  27294  2lgsoddprmlem3c  27321  rplogsum  27436  mulog2sumlem2  27444  pnt2  27522  bdayfo  27587  bday0s  27742  bday1s  27745  old1  27789  addsasslem2  27916  negsbdaylem  27967  muls01  28020  abssnid  28150  1p1e2s  28308  n0seo  28313  twocut  28315  halfcut  28346  pw2cutp1  28349  zs12bday  28361  istrkg2ld  28405  axsegconlem9  28870  ax5seglem7  28880  iedgedg  28995  uspgrf1oedg  29118  nbgrcl  29280  nbgrnvtx0  29284  rusgrprc  29536  pthsfval  29664  wlkiswwlks2lem4  29817  wlkiswwlks2lem5  29818  clwwlkvbij  30057  konigsbergumgr  30195  ex-pw  30373  ex-xp  30380  ex-rn  30384  nvvop  30553  nvm  30585  cnims  30637  ip0i  30769  ip1ilem  30770  ipdirilem  30773  ipasslem10  30783  h2hva  30918  h2hsm  30919  h2hvs  30921  axhfvadd-zf  30926  axhvcom-zf  30927  axhvass-zf  30928  axhv0cl-zf  30929  axhvaddid-zf  30930  axhfvmul-zf  30931  axhvmulid-zf  30932  axhvmulass-zf  30933  axhvdistr1-zf  30934  axhvdistr2-zf  30935  axhvmul0-zf  30936  axhfi-zf  30937  axhis1-zf  30938  axhis2-zf  30939  axhis3-zf  30940  axhis4-zf  30941  axhcompl-zf  30942  normlem0  31053  normlem1  31054  normlem2  31055  normlem4  31057  normlem9  31062  bcseqi  31064  dfhnorm2  31066  norm3difi  31091  normpari  31098  normpar2i  31100  polid2i  31101  polidi  31102  hhba  31111  hhims  31116  hhims2  31117  hhsssh  31213  hhssims  31218  hhssims2  31219  shsval3i  31332  dfch2  31351  cmcm2i  31537  fh2  31563  qlaxr3i  31580  spansnji  31590  pjcji  31628  ho0val  31694  df0op2  31696  hosd1i  31766  hosd2i  31767  eigorthi  31781  hhlnoi  31844  hhnmoi  31845  hhbloi  31846  bra0  31894  nmop0  31930  nmfn0  31931  lnopeq0lem1  31949  lnopunilem1  31954  lnophmlem2  31961  nmopcoadji  32045  pjhmopidm  32127  cvmdi  32268  cdj3lem3  32382  cdj3lem3b  32384  abrexdomjm  32451  uniin1  32495  uniin2  32496  iundifdifd  32505  iundifdif  32506  mpomptxf  32620  df1stres  32646  df2ndres  32647  intimafv  32653  fcobijfs  32665  fcobijfs2  32666  resf1o  32673  fpwrelmapffslem  32675  sgnneg  32778  dpval3  32834  dp3mul10  32838  dpadd2  32850  dpmul4  32854  ccatws1f1o  32893  chnub  32954  xrslt  32961  xrsclat  32965  xrge0tsmsd  33015  cycpmco2lem7  33074  cycpmconjv  33084  cycpmrn  33085  conjga  33112  elrgspnsubrunlem2  33188  rndrhmcl  33235  fracf1  33246  xrge0slmod  33285  lsmsnorb2  33329  qusbas2  33343  1arithidomlem2  33473  zringfrac  33491  mplvrpmga  33546  rlmdim  33576  rgmoddimOLD  33577  isconstr  33703  iconstr  33733  cos9thpiminplylem4  33752  cos9thpiminplylem5  33753  circtopn  33804  tpr2rico  33879  xrge0mulc1cn  33908  lmxrge0  33919  esumpfinvallem  34041  esumcocn  34047  hasheuni  34052  esumcvg  34053  rossros  34147  measinblem  34187  aean  34211  sxbrsigalem3  34240  dya2iocival  34241  dya2iocucvr  34252  sxbrsigalem1  34253  sxbrsigalem2  34254  sxbrsigalem5  34256  sxbrsiga  34258  fiunelcarsg  34284  eulerpartlem1  34335  eulerpartgbij  34340  fibp1  34369  coinfliplem  34447  coinflipprob  34448  ballotlemfval  34458  ballotth  34506  plymulx  34516  circlemethhgt  34611  hgt750lem2  34620  bnj1400  34802  bnj66  34827  bnj882  34893  lfuhgr  35095  derang0  35146  subfacp1lem1  35156  subfacp1lem6  35162  kur14lem7  35189  cvmsss2  35251  cvmliftlem8  35269  cvmliftlem10  35271  satfv1lem  35339  msubfval  35501  quad3  35647  bcprod  35715  bccolsum  35716  faclim  35723  pprodcnveq  35861  dfon4  35871  fobigcup  35878  dfiota3  35901  dfrecs2  35928  dfrdg4  35929  dfint3  35930  rankeq1o  36149  refssfne  36336  ssoninhaus  36426  onint1  36427  bj-rababw  36859  bj-inrab3  36907  bj-imdiridlem  37163  dissneq  37319  dffinxpf  37363  finxpreclem4  37372  rabiun  37577  ptrest  37603  poimirlem3  37607  poimirlem4  37608  poimirlem13  37617  poimirlem16  37620  poimirlem22  37626  poimirlem26  37630  poimirlem27  37631  poimirlem30  37634  cnambfre  37652  ftc1anclem8  37684  fnopabco  37707  abrexdom  37714  cncfres  37749  scottexf  38152  scott0f  38153  inres2  38224  dfres4  38271  dmxrn  38350  xrnres  38378  xrnres2  38379  dfcoss2  38394  dfcoss4  38396  1cossres  38410  dmcoss2  38435  1cosscnvxrn  38456  dfeqvrels2  38569  dfcoeleqvrels  38602  redundss3  38609  dffunsALTV5  38669  cdleme3d  40214  cdleme7a  40226  cdleme31sdnN  40370  cdlemk45  40930  420gcd8e4  41983  lcmeprodgcdi  41984  60lcm7e420  41987  420lcm8e840  41988  3lexlogpow5ineq1  42031  3lexlogpow2ineq1  42035  3lexlogpow2ineq2  42036  3lexlogpow5ineq5  42037  aks4d1p1  42053  posbezout  42077  aks6d1c1p4  42088  aks6d1c3  42100  2ap1caineq  42122  sticksstones7  42129  sticksstones12a  42134  sticksstones12  42135  aks6d1c6lem4  42150  imaopab  42208  fmpocos  42211  dfqs2  42214  dfqs3  42215  decaddcom  42261  sumcubes  42290  redvmptabs  42337  readvrec  42339  readvcot  42341  sn-00idlem2  42376  reixi  42400  sum9cubes  42649  mapfzcons  42693  eldioph4b  42788  diophren  42790  pwssplit4  43066  pwfi2f1o  43073  frlmpwfi  43075  mendplusgfval  43158  mendmulrfval  43160  mendvscafval  43163  idomodle  43168  cytpval  43179  arearect  43192  onov0suclim  43251  omabs2  43309  tr3dom  43505  har2o  43523  alephiso2  43535  alephiso3  43536  relintab  43560  dfid7  43589  cnvrcl0  43602  dfrtrcl5  43606  dfrcl3  43652  dfrcl4  43653  comptiunov2i  43683  corcltrcl  43716  neicvgnvo  44092  inductionexd  44132  mnuprdlem2  44250  nznngen  44293  hashnzfz2  44298  lhe4.4ex1a  44306  dvradcnv2  44324  binomcxplemrat  44327  binomcxplemnotnn0  44333  nregmodelf1o  44993  refsum2cnlem1  45019  fiiuncl  45047  iccdifprioo  45501  lptre2pt  45625  limclner  45636  stoweidlem13  45998  stoweidlem32  46017  stoweidlem62  46047  wallispi2lem2  46057  stirlinglem14  46072  dirkertrigeqlem1  46083  dirkercncflem4  46091  fourierdlem42  46134  fourierdlem73  46164  fourierdlem81  46172  fourierdlem92  46183  fourierdlem103  46194  fourierdlem104  46195  fouriercnp  46211  fouriersw  46216  sge0tsms  46365  sge0iunmptlemfi  46398  ovolval5lem3  46639  cnfsmf  46725  lamberte  46876  rnfdmpr  47269  fvmptrabdm  47281  fundcmpsurinjlem1  47386  m11nprm  47589  opoeALTV  47671  nfermltl8rev  47730  sbgoldbo  47775  evengpop3  47786  clnbgrcl  47809  clnbgrnvtx0  47815  usgrexmpl2edg  48017  usgrexmpl2nb0  48019  usgrexmpl2nb3  48022  gpg5order  48048  gpgprismgr4cycllem6  48088  cznabel  48248  cznrng  48249  mpomptx2  48323  2sphere  48738  itscnhlinecirc02plem3  48773  inlinecirc02p  48776  dftpos5  48862  tposresg  48866  icccldii  48907  dfnrm2  48920  dfnrm3  48921  elxpcbasex1ALT  49238  elxpcbasex2ALT  49240  dfswapf2  49250  swapf1a  49258  swapf1f1o  49264  swapf2f1oa  49266  swapfida  49269  setc1oterm  49480  setc1ohomfval  49482  setc1ocofval  49483  funcsetc1o  49486  dfinito4  49490  setc1onsubc  49591  islmd  49654  iscmd  49655  initocmd  49658  termolmd  49659  amgmlemALT  49792