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 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  3eqtr2i  2792  3eqtr2ri  2793  3eqtr4i  2796  3eqtr4ri  2797  rabab  3485  cbvralcsf  3895  cbvrabcsf  3898  dfin5  3913  dfdif2  3914  uneqin  4242  notabw  4266  unrab  4268  inrab  4269  inrab2  4270  difrab  4271  dfrab3ss  4276  rabun2  4277  dfnul2  4289  difid  4332  rabxm  4347  elnelun  4350  abf  4371  difdifdir  4452  dfif3  4502  dfif5  4504  rabsnif  4689  tpidm  4724  ssunpr  4799  sstp  4801  opidg  4857  dfint2  4914  iunrab  5017  uniiun  5023  intiin  5024  iunid  5025  0iin  5028  uniin1  5039  uniin2  5040  mptv  5217  dfepfr  5645  epfrc  5646  xpundi  5730  xpundir  5731  csbcnv  5872  csbcnvOLD  5873  resiun2  5999  resopab  6036  mptresid  6053  dffr3  6101  dfse2  6102  cnvun  6139  imaundir  6148  imainrect  6179  cnvcnv2  6191  cnvrescnv  6194  cnvcnvres  6206  dmtpop  6219  rnsnopg  6222  resdifdi  6237  rnco2  6255  dmco  6256  co01  6263  unidmrn  6280  dfdm2  6282  predidm  6327  dfmpt3  6669  mptun  6681  funcocnv2  6846  dffv2  6976  fnasrn  7141  fpr  7151  fmptap  7168  rnmptc  7205  riotav  7372  dmoprab  7513  rnoprab2  7516  mpov  7522  mpomptx  7523  abrexex2g  7957  1stval2  7999  2ndval2  8000  fo1st  8002  fo2nd  8003  xp2  8019  dfoprab4f  8049  offval22  8079  fmpoco  8086  fimaproj  8127  tposmpo  8255  tposconst  8256  recsfval  8363  rdgsucmpt2  8413  frsucmpt2  8423  df2o3  8457  o1p1e2  8521  o2p2e4  8522  oarec  8543  omopthlem2  8642  dfqs2  8697  ecqs  8773  qliftf  8799  erovlem  8807  fset0  8847  mapsnf1o3  8889  ixp0x  8920  omf1o  9064  xpf1o  9123  mapunen  9130  enp1ilem  9234  marypha1lem  9389  marypha2lem4  9394  dfoi  9469  infeq5i  9601  oemapso  9647  cantnflem1  9654  rankelop  9842  leweon  9991  r0weon  9992  kmlem11  10140  dju1dif  10152  ackbij1lem16  10213  cf0  10229  cfsmolem  10249  alephsuc3  10560  fpwwe  10626  canthp1lem1  10632  wuncval2  10727  prlem936  11027  m1p1sr  11072  m1m1sr  11073  dfcnqs  11122  ssxr  11274  mul02lem2  11382  addrid  11385  2p2e4  12370  3p2e5  12386  3p3e6  12387  4p2e6  12388  4p3e7  12389  4p4e8  12390  5p2e7  12391  5p3e8  12392  5p4e9  12393  6p2e8  12394  6p3e9  12395  7p2e9  12396  nnzrab  12617  nn0zrab  12618  dec0u  12732  dec0h  12733  decsuc  12742  decsucc  12752  numma  12755  decma  12762  decmac  12763  decma2c  12764  decadd  12765  decaddc  12766  decmul1c  12776  decmul2c  12777  5p5e10  12782  6p4e10  12783  7p3e10  12786  8p2e10  12791  5t5e25  12814  6t6e36  12819  8t6e48  12830  nn0uz  12895  nnuz  12896  xaddcom  13261  x2times  13320  ioomax  13444  iccmax  13445  ioopos  13446  ioorp  13447  prunioo  13503  fseq1p1m1  13622  fzo13pr  13774  fzo0to2pr  13775  fzo0to3tp  13777  om2uzrdg  13988  fzennn  14000  irec  14233  sq10e99m1  14297  facnn  14307  fac0  14308  faclbnd2  14323  faclbnd4lem1  14325  hashfun  14470  hashbclem  14485  hashf1lem1  14488  hashf1lem2  14489  fz1isolem  14494  swrdccatin1  14758  swrdccat3blem  14772  s1co  14866  s2eq2s1eq  14969  s3eqs2s1eq  14971  ofs2  15004  dfid5  15060  dfid6  15061  sgnneg  15133  fsumrev2  15829  fsumparts  15854  fsumiun  15869  isumnn0nn  15892  harmonic  15909  fprod2d  16031  bpoly2  16106  bpoly3  16107  bpoly4  16108  ege2le3  16139  cos1bnd  16238  efieq1re  16250  eirrlem  16255  qnnen  16264  cpnnen  16280  ruclem6  16286  3dvds  16384  pwp1fsum  16444  m1bits  16493  nn0expgcd  16617  algrp1  16627  phiprmpw  16830  prmreclem4  16974  4sqlem11  17010  4sqlem19  17018  dec5dvds  17119  decsplit1  17136  5prm  17163  7prm  17165  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  1259prm  17191  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  4001prm  17200  strle1  17213  grpbasex  17340  grpplusgx  17341  quslem  17592  xpsrnbas  17620  acsfn1  17712  acsfn2  17714  comfffval2  17752  dfinito2  18055  dftermo2  18056  xpchomfval  18230  xpccofval  18233  1stfval  18242  2ndfval  18245  oduleg  18341  chnub  18673  ismgmid  18718  efmndbas  18925  smndex2dnrinv  18972  grpinvfvi  19044  gaorb  19372  elcntr  19395  cntri  19397  cntrsubgnsg  19408  cntrnsg  19409  setsplusg  19415  oppgcntr  19430  gsumwrev  19431  symgressbas  19447  symgplusg  19448  symgvalstruct  19462  symgga  19472  cayleylem1  19477  psgnunilem2  19560  efgval2  19789  efgredlemc  19810  efgcpbllema  19819  frgpnabllem1  19938  gsumzaddlem  19986  gsumle  20210  opprlem  20420  oppr0  20427  opprneg  20429  rmodislmod  21051  rlmscaf  21328  xrsds  21560  gsumfsum  21584  zringunit  21616  pzriprng1  21648  cnmsgngrp  21729  psgnfix2  21749  relt  21765  ocv0  21827  thlle  21847  thlleval  21848  dsmmval2  21886  frlmip  21928  mplbas  22139  mplplusg  22156  mplmulr  22157  mplvsca2  22163  ressmplbas2  22177  ltbwe  22195  evlslem4  22227  psdmul  22329  psr1bas2  22350  ply1bas  22355  ply1assa  22359  psr1plusg  22380  psr1vsca  22381  psr1mulr  22382  ply1plusg  22383  ply1vsca  22384  ply1mulr  22385  ply1mpl0  22416  ply1mpl1  22418  coe1mul  22431  matgsum  22594  smadiadetglem1  22828  indistpsx  23167  iuncld  23202  tgrest  23316  resstopn  23343  leordtval2  23369  xkouni  23756  ptclsg  23772  ptuncnv  23964  ptunhmeo  23965  alexsubALTlem4  24207  tsmsf1o  24302  ucnimalem  24436  ressxms  24682  uniretop  24919  cnfldtopn  24938  xrtgioo  24964  zcld  24971  icccmp  24983  xrge0gsumle  24991  xrge0tsms  24992  metnrmlem3  25019  fsum2cn  25030  cnmpopc  25087  oprpiece1res1  25110  oprpiece1res2  25111  evth  25118  evth2  25119  om1opn  25195  pi1xfrf  25212  pi1xfrcnv  25216  pi1cof  25218  clsocv  25409  cncmet  25481  cnflduss  25515  rrxprds  25548  ehlbase  25574  ismbl  25685  shftmbl  25697  ioorinv  25735  itg1addlem4  25858  itg2cnlem1  25920  itg0  25939  itgss3  25974  ditgneg  26016  limcdif  26035  limciun  26053  dvexp  26112  dvef  26139  dvcnvrelem2  26177  ftc1  26201  plymulidp  26443  aannenlem2  26492  dvradcnv  26584  pserdvlem2  26591  reefgim  26613  cospi  26637  sincos6thpi  26681  tanregt0  26704  dflog2  26725  logfac  26766  dvlog  26816  cxpexp  26833  cxpmul2  26854  cxpsqrt  26868  dvsqrt  26907  dvcnsqrt  26909  cxpcn2  26911  isosctrlem2  26984  1cubrlem  27006  1cubr  27007  quart1lem  27020  atancj  27075  atanlogaddlem  27078  atansopn  27097  leibpilem2  27106  log2cnv  27109  log2ublem3  27113  birthdaylem1  27116  birthdaylem2  27117  birthday  27119  dfarea  27125  lgamgulmlem5  27197  lgambdd  27201  ftalem3  27239  basellem2  27246  ppiprm  27315  ppinprm  27316  chtprm  27317  chtnprm  27318  ppi2  27334  ppi3  27335  ppiub  27368  chtub  27376  bclbnd  27444  bposlem8  27455  lgsdilem  27488  lgsdir2lem2  27490  lgsquadlem2  27545  lgsquad2lem2  27549  2lgsoddprmlem3c  27576  rplogsum  27691  mulog2sumlem2  27699  pnt2  27777  bdayfo  27841  bday0  28004  bday1  28007  old1  28058  addsasslem2  28197  negbdaylem  28249  muls01  28305  abssnid  28436  1p1e2s  28609  n0seo  28614  twocut  28616  halfcut  28651  pw2cutp1  28654  pw2cut2  28655  istrkg2ld  28729  axsegconlem9  29275  ax5seglem7  29285  iedgedg  29400  uspgrf1oedg  29523  nbgrcl  29685  nbgrnvtx0  29689  rusgrprc  29940  pthsfval  30068  wlkiswwlks2lem4  30221  wlkiswwlks2lem5  30222  clwwlkvbij  30464  konigsbergumgr  30602  ex-pw  30780  ex-xp  30787  ex-rn  30791  nvvop  30961  nvm  30993  cnims  31045  ip0i  31177  ip1ilem  31178  ipdirilem  31181  ipasslem10  31191  h2hva  31326  h2hsm  31327  h2hvs  31329  axhfvadd-zf  31334  axhvcom-zf  31335  axhvass-zf  31336  axhv0cl-zf  31337  axhvaddid-zf  31338  axhfvmul-zf  31339  axhvmulid-zf  31340  axhvmulass-zf  31341  axhvdistr1-zf  31342  axhvdistr2-zf  31343  axhvmul0-zf  31344  axhfi-zf  31345  axhis1-zf  31346  axhis2-zf  31347  axhis3-zf  31348  axhis4-zf  31349  axhcompl-zf  31350  normlem0  31461  normlem1  31462  normlem2  31463  normlem4  31465  normlem9  31470  bcseqi  31472  dfhnorm2  31474  norm3difi  31499  normpari  31506  normpar2i  31508  polid2i  31509  polidi  31510  hhba  31519  hhims  31524  hhims2  31525  hhsssh  31621  hhssims  31626  hhssims2  31627  shsval3i  31740  dfch2  31759  cmcm2i  31945  fh2  31971  qlaxr3i  31988  spansnji  31998  pjcji  32036  ho0val  32102  df0op2  32104  hosd1i  32174  hosd2i  32175  eigorthi  32189  hhlnoi  32252  hhnmoi  32253  hhbloi  32254  bra0  32302  nmop0  32338  nmfn0  32339  lnopeq0lem1  32357  lnopunilem1  32362  lnophmlem2  32369  nmopcoadji  32453  pjhmopidm  32535  cvmdi  32676  cdj3lem3  32790  cdj3lem3b  32792  abrexdomjm  32853  iundifdifd  32906  iundifdif  32907  mpomptxf  33023  df1stres  33049  df2ndres  33050  intimafv  33056  fcobijfs  33066  fcobijfs2  33067  resf1o  33075  fpwrelmapffslem  33077  dpval3  33213  dp3mul10  33217  dpadd2  33229  dpmul4  33233  ccatws1f1o  33271  xrslt  33327  xrsclat  33331  xrge0tsmsd  33393  cycpmco2lem7  33452  cycpmconjv  33462  cycpmrn  33463  conjga  33490  elrgspnsubrunlem2  33568  rndrhmcl  33617  fracf1  33628  xrge0slmod  33668  lsmsnorb2  33705  qusbas2  33715  1arithidomlem2  33826  zringfrac  33844  selvply1rhm0  33916  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  psrmonprod  33942  mplmonprod  33944  vieta  33970  rlmdim  34000  isconstr  34126  iconstr  34156  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  circtopn  34227  tpr2rico  34302  xrge0mulc1cn  34331  lmxrge0  34342  esumpfinvallem  34464  esumcocn  34470  hasheuni  34475  esumcvg  34476  rossros  34570  measinblem  34610  aean  34634  sxbrsigalem3  34662  dya2iocival  34663  dya2iocucvr  34674  sxbrsigalem1  34675  sxbrsigalem2  34676  sxbrsigalem5  34678  sxbrsiga  34680  fiunelcarsg  34706  eulerpartlem1  34757  eulerpartgbij  34762  fibp1  34791  coinfliplem  34869  coinflipprob  34870  ballotlemfval  34880  ballotth  34928  circlemethhgt  35030  hgt750lem2  35039  bnj1400  35223  bnj66  35248  bnj882  35314  dfscott2  35511  dfscott3  35512  lfuhgr  35610  derang0  35661  subfacp1lem1  35671  subfacp1lem6  35677  kur14lem7  35704  cvmsss2  35766  cvmliftlem8  35784  cvmliftlem10  35786  satfv1lem  35854  msubfval  36016  quad3  36162  bcprod  36230  bccolsum  36231  faclim  36238  pprodcnveq  36373  dfon4  36383  fobigcup  36390  dfiota3  36413  dfrecs2  36442  dfrdg4  36443  dfint3  36444  rankeq1o  36663  refssfne  36869  ssoninhaus  36959  onint1  36960  ttciun  37025  bj-dfnul2  37163  bj-rababw  37516  bj-inrab3  37565  bj-imdiridlem  37829  dissneq  37987  dffinxpf  38031  finxpreclem4  38040  rabiun  38244  ptrest  38270  poimirlem3  38274  poimirlem4  38275  poimirlem13  38284  poimirlem16  38287  poimirlem22  38293  poimirlem26  38297  poimirlem27  38298  poimirlem30  38301  cnambfre  38319  ftc1anclem8  38351  fnopabco  38374  abrexdom  38381  cncfres  38416  scottexf  38817  scott0f  38818  inres2  38896  eqrabi  38905  xpv  38911  dfres4  38948  dmxrn  39036  xrnres  39074  xrnres2  39075  rnqmap  39103  dfsucmap2  39113  dfcoss2  39152  dfcoss4  39154  1cossres  39168  dmcoss2  39193  1cosscnvxrn  39214  dfeqvrels2  39321  dfcoeleqvrels  39354  redundss3  39361  dffunsALTV5  39421  dfpeters2  39623  cdleme3d  41005  cdleme7a  41017  cdleme31sdnN  41161  cdlemk45  41721  420gcd8e4  42773  lcmeprodgcdi  42774  60lcm7e420  42777  420lcm8e840  42778  3lexlogpow5ineq1  42821  3lexlogpow2ineq1  42825  3lexlogpow2ineq2  42826  3lexlogpow5ineq5  42827  aks4d1p1  42843  posbezout  42867  aks6d1c1p4  42878  aks6d1c3  42890  2ap1caineq  42912  sticksstones7  42919  sticksstones12a  42924  sticksstones12  42925  aks6d1c6lem4  42940  25or6to4  42973  imaopab  43002  fmpocos  43004  dfqs3  43007  decaddcom  43045  sumcubes  43074  redvmptabs  43121  readvrec  43123  readvcot  43125  sn-00idlem2  43160  reixi  43184  sum9cubes  43404  mapfzcons  43447  eldioph4b  43538  diophren  43540  pwssplit4  43816  pwfi2f1o  43823  frlmpwfi  43825  mendplusgfval  43908  mendmulrfval  43910  mendvscafval  43913  idomodle  43918  cytpval  43929  arearect  43942  onov0suclim  44001  omabs2  44059  tr3dom  44254  har2o  44272  alephiso2  44284  alephiso3  44285  relintab  44309  dfid7  44338  cnvrcl0  44351  dfrtrcl5  44355  dfrcl3  44401  dfrcl4  44402  comptiunov2i  44432  corcltrcl  44465  neicvgnvo  44841  inductionexd  44881  mnuprdlem2  44983  nznngen  45026  hashnzfz2  45031  lhe4.4ex1a  45039  dvradcnv2  45057  binomcxplemrat  45060  binomcxplemnotnn0  45066  nregmodelf1o  45724  refsum2cnlem1  45757  fiiuncl  45785  iccdifprioo  46232  lptre2pt  46354  limclner  46365  stoweidlem13  46727  stoweidlem32  46746  stoweidlem62  46776  wallispi2lem2  46786  stirlinglem14  46801  dirkertrigeqlem1  46812  dirkercncflem4  46820  fourierdlem42  46863  fourierdlem73  46893  fourierdlem81  46901  fourierdlem92  46912  fourierdlem103  46923  fourierdlem104  46924  fouriercnp  46940  fouriersw  46945  sge0tsms  47094  sge0iunmptlemfi  47127  ovolval5lem3  47368  cnfsmf  47454  lamberte  47625  rnfdmpr  48018  fvmptrabdm  48030  fundcmpsurinjlem1  48147  m11nprm  48353  ppi1sum  48383  opoeALTV  48448  nfermltl8rev  48507  sbgoldbo  48552  evengpop3  48563  clnbgrcl  48586  clnbgrnvtx0  48592  usgrexmpl2edg  48794  usgrexmpl2nb0  48796  usgrexmpl2nb3  48799  gpg5order  48825  gpgprismgr4cycllem6  48865  cznabel  49025  cznrng  49026  mpomptx2  49115  2sphere  49529  itscnhlinecirc02plem3  49564  inlinecirc02p  49567  dftpos5  49652  tposresg  49656  icccldii  49697  dfnrm2  49710  dfnrm3  49711  elxpcbasex1ALT  50027  elxpcbasex2ALT  50029  dfswapf2  50039  swapf1a  50047  swapf1f1o  50053  swapf2f1oa  50055  swapfida  50058  setc1oterm  50269  setc1ohomfval  50271  setc1ocofval  50272  funcsetc1o  50275  dfinito4  50279  setc1onsubc  50380  islmd  50443  iscmd  50444  initocmd  50447  termolmd  50448  amgmlemALT  50623