Theorem eqtr4i 2760

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 2743	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2757	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 2123  ax-ext 2706

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

This theorem is referenced by:  3eqtr2i  2763  3eqtr2ri  2764  3eqtr4i  2767  3eqtr4ri  2768  rabab  3469  cbvralcsf  3889  cbvrabcsf  3892  dfin5  3907  dfdif2  3908  uneqin  4239  notabw  4263  unrab  4265  inrab  4266  inrab2  4267  difrab  4268  dfrab3ss  4273  rabun2  4274  dfnul2  4286  difid  4326  rabxm  4340  elnelun  4343  abf  4356  difdifdir  4442  dfif3  4492  dfif5  4494  rabsnif  4678  tpidm  4713  ssunpr  4788  sstp  4790  opidg  4846  dfint2  4902  iunrab  5006  uniiun  5012  intiin  5013  iunid  5014  0iin  5017  mptv  5202  dfepfr  5606  epfrc  5607  xpundi  5691  xpundir  5692  csbcnv  5830  resiun2  5957  resopab  5991  mptresid  6008  dffr3  6056  dfse2  6057  cnvun  6098  imaundir  6106  imainrect  6137  cnvcnv2  6149  cnvrescnv  6151  cnvcnvres  6161  dmtpop  6174  rnsnopg  6177  resdifdi  6192  rnco2  6210  dmco  6211  co01  6218  unidmrn  6235  dfdm2  6237  predidm  6282  dfmpt3  6624  mptun  6636  funcocnv2  6797  dffv2  6927  fnasrn  7088  fpr  7097  fmptap  7114  rnmptc  7151  riotav  7318  dmoprab  7459  rnoprab2  7462  mpov  7468  mpomptx  7469  abrexex2g  7906  1stval2  7948  2ndval2  7949  fo1st  7951  fo2nd  7952  xp2  7968  dfoprab4f  7998  offval22  8028  fmpoco  8035  fimaproj  8075  tposmpo  8203  tposconst  8204  recsfval  8310  rdgsucmpt2  8359  frsucmpt2  8369  df2o3  8403  o1p1e2  8465  o2p2e4  8466  oarec  8487  omopthlem2  8586  ecqs  8714  qliftf  8740  erovlem  8748  fset0  8789  mapsnf1o3  8831  ixp0x  8862  omf1o  9006  xpf1o  9065  mapunen  9072  enp1ilem  9176  marypha1lem  9334  marypha2lem4  9339  dfoi  9414  infeq5i  9543  oemapso  9589  cantnflem1  9596  rankelop  9784  leweon  9919  r0weon  9920  kmlem11  10069  dju1dif  10081  ackbij1lem16  10142  cf0  10159  cfsmolem  10178  alephsuc3  10489  fpwwe  10555  canthp1lem1  10561  wuncval2  10656  prlem936  10956  m1p1sr  11001  m1m1sr  11002  dfcnqs  11051  ssxr  11200  mul02lem2  11308  addrid  11311  2p2e4  12273  3p2e5  12289  3p3e6  12290  4p2e6  12291  4p3e7  12292  4p4e8  12293  5p2e7  12294  5p3e8  12295  5p4e9  12296  6p2e8  12297  6p3e9  12298  7p2e9  12299  nnzrab  12517  nn0zrab  12518  dec0u  12626  dec0h  12627  decsuc  12636  decsucc  12646  numma  12649  decma  12656  decmac  12657  decma2c  12658  decadd  12659  decaddc  12660  decmul1c  12670  decmul2c  12671  5p5e10  12676  6p4e10  12677  7p3e10  12680  8p2e10  12685  5t5e25  12708  6t6e36  12713  8t6e48  12724  nn0uz  12787  nnuz  12788  xaddcom  13153  x2times  13212  ioomax  13336  iccmax  13337  ioopos  13338  ioorp  13339  prunioo  13395  fseq1p1m1  13512  fzo13pr  13663  fzo0to2pr  13664  fzo0to3tp  13666  om2uzrdg  13877  fzennn  13889  irec  14122  sq10e99m1  14186  facnn  14196  fac0  14197  faclbnd2  14212  faclbnd4lem1  14214  hashfun  14358  hashbclem  14373  hashf1lem1  14376  hashf1lem2  14377  fz1isolem  14382  swrdccatin1  14646  swrdccat3blem  14660  s1co  14754  s2eq2s1eq  14857  s3eqs2s1eq  14859  ofs2  14892  dfid5  14948  dfid6  14949  fsumrev2  15703  fsumparts  15727  fsumiun  15742  isumnn0nn  15763  harmonic  15780  fprod2d  15902  bpoly2  15978  bpoly3  15979  bpoly4  15980  ege2le3  16011  cos1bnd  16110  efieq1re  16122  eirrlem  16127  qnnen  16136  cpnnen  16152  ruclem6  16158  3dvds  16256  pwp1fsum  16316  m1bits  16365  nn0expgcd  16489  algrp1  16499  phiprmpw  16701  prmreclem4  16845  4sqlem11  16881  4sqlem19  16889  dec5dvds  16990  decsplit1  17007  5prm  17034  7prm  17036  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  4001prm  17070  strle1  17083  grpbasex  17210  grpplusgx  17211  quslem  17462  xpsrnbas  17490  acsfn1  17582  acsfn2  17584  comfffval2  17622  dfinito2  17925  dftermo2  17926  xpchomfval  18100  xpccofval  18103  1stfval  18112  2ndfval  18115  oduleg  18211  chnub  18543  ismgmid  18588  efmndbas  18794  smndex2dnrinv  18838  grpinvfvi  18910  gaorb  19234  elcntr  19257  cntri  19259  cntrsubgnsg  19270  cntrnsg  19271  setsplusg  19277  oppgcntr  19292  gsumwrev  19293  symgressbas  19309  symgplusg  19310  symgvalstruct  19324  symgga  19334  cayleylem1  19339  psgnunilem2  19422  efgval2  19651  efgredlemc  19672  efgcpbllema  19681  frgpnabllem1  19800  gsumzaddlem  19848  gsumle  20072  opprlem  20276  oppr0  20283  opprneg  20285  rmodislmod  20879  rlmscaf  21157  xrsds  21362  gsumfsum  21387  zringunit  21419  pzriprng1  21451  cnmsgngrp  21532  psgnfix2  21552  relt  21568  ocv0  21630  thlle  21650  thlleval  21651  dsmmval2  21689  frlmip  21731  mplbas  21943  mplplusg  21960  mplmulr  21961  mplvsca2  21967  ressmplbas2  21980  ltbwe  21997  evlslem4  22029  psdmul  22107  psr1bas2  22128  ply1bas  22133  ply1basOLD  22134  ply1assa  22138  psr1plusg  22159  psr1vsca  22160  psr1mulr  22161  ply1plusg  22162  ply1vsca  22163  ply1mulr  22164  ply1mpl0  22195  ply1mpl1  22197  coe1mul  22210  matgsum  22379  smadiadetglem1  22613  indistpsx  22952  iuncld  22987  tgrest  23101  resstopn  23128  leordtval2  23154  xkouni  23541  ptclsg  23557  ptuncnv  23749  ptunhmeo  23750  alexsubALTlem4  23992  tsmsf1o  24087  ucnimalem  24221  ressxms  24467  uniretop  24704  cnfldtopn  24723  xrtgioo  24749  zcld  24756  icccmp  24768  xrge0gsumle  24776  xrge0tsms  24777  metnrmlem3  24804  fsum2cn  24816  cnmpopc  24876  oprpiece1res1  24903  oprpiece1res2  24904  evth  24912  evth2  24913  om1opn  24990  pi1xfrf  25007  pi1xfrcnv  25011  pi1cof  25013  clsocv  25204  cncmet  25276  cnflduss  25310  rrxprds  25343  ehlbase  25369  ismbl  25481  shftmbl  25493  ioorinv  25531  itg1addlem4  25654  itg2cnlem1  25716  itg0  25735  itgss3  25770  ditgneg  25812  limcdif  25831  limciun  25849  dvexp  25911  dvef  25938  dvcnvrelem2  25977  ftc1  26003  aannenlem2  26291  dvradcnv  26384  pserdvlem2  26392  reefgim  26414  cospi  26435  sincos6thpi  26479  tanregt0  26502  dflog2  26523  logfac  26564  dvlog  26614  cxpexp  26631  cxpmul2  26652  cxpsqrt  26666  dvsqrt  26705  dvcnsqrt  26707  cxpcn2  26710  isosctrlem2  26783  1cubrlem  26805  1cubr  26806  quart1lem  26819  atancj  26874  atanlogaddlem  26877  atansopn  26896  leibpilem2  26905  log2cnv  26908  log2ublem3  26912  birthdaylem1  26915  birthdaylem2  26916  birthday  26918  dfarea  26924  lgamgulmlem5  26997  lgambdd  27001  ftalem3  27039  basellem2  27046  ppiprm  27115  ppinprm  27116  chtprm  27117  chtnprm  27118  ppi2  27134  ppi3  27135  ppiub  27169  chtub  27177  bclbnd  27245  bposlem8  27256  lgsdilem  27289  lgsdir2lem2  27291  lgsquadlem2  27346  lgsquad2lem2  27350  2lgsoddprmlem3c  27377  rplogsum  27492  mulog2sumlem2  27500  pnt2  27578  bdayfo  27643  bday0s  27799  bday1s  27802  old1  27847  addsasslem2  27974  negsbdaylem  28025  muls01  28081  abssnid  28211  1p1e2s  28374  n0seo  28379  twocut  28381  halfcut  28415  pw2cutp1  28418  pw2cut2  28419  zs12bday  28433  istrkg2ld  28481  axsegconlem9  28947  ax5seglem7  28957  iedgedg  29072  uspgrf1oedg  29195  nbgrcl  29357  nbgrnvtx0  29361  rusgrprc  29613  pthsfval  29741  wlkiswwlks2lem4  29894  wlkiswwlks2lem5  29895  clwwlkvbij  30137  konigsbergumgr  30275  ex-pw  30453  ex-xp  30460  ex-rn  30464  nvvop  30633  nvm  30665  cnims  30717  ip0i  30849  ip1ilem  30850  ipdirilem  30853  ipasslem10  30863  h2hva  30998  h2hsm  30999  h2hvs  31001  axhfvadd-zf  31006  axhvcom-zf  31007  axhvass-zf  31008  axhv0cl-zf  31009  axhvaddid-zf  31010  axhfvmul-zf  31011  axhvmulid-zf  31012  axhvmulass-zf  31013  axhvdistr1-zf  31014  axhvdistr2-zf  31015  axhvmul0-zf  31016  axhfi-zf  31017  axhis1-zf  31018  axhis2-zf  31019  axhis3-zf  31020  axhis4-zf  31021  axhcompl-zf  31022  normlem0  31133  normlem1  31134  normlem2  31135  normlem4  31137  normlem9  31142  bcseqi  31144  dfhnorm2  31146  norm3difi  31171  normpari  31178  normpar2i  31180  polid2i  31181  polidi  31182  hhba  31191  hhims  31196  hhims2  31197  hhsssh  31293  hhssims  31298  hhssims2  31299  shsval3i  31412  dfch2  31431  cmcm2i  31617  fh2  31643  qlaxr3i  31660  spansnji  31670  pjcji  31708  ho0val  31774  df0op2  31776  hosd1i  31846  hosd2i  31847  eigorthi  31861  hhlnoi  31924  hhnmoi  31925  hhbloi  31926  bra0  31974  nmop0  32010  nmfn0  32011  lnopeq0lem1  32029  lnopunilem1  32034  lnophmlem2  32041  nmopcoadji  32125  pjhmopidm  32207  cvmdi  32348  cdj3lem3  32462  cdj3lem3b  32464  abrexdomjm  32531  uniin1  32575  uniin2  32576  iundifdifd  32585  iundifdif  32586  mpomptxf  32706  df1stres  32732  df2ndres  32733  intimafv  32739  fcobijfs  32749  fcobijfs2  32750  resf1o  32758  fpwrelmapffslem  32760  sgnneg  32863  dpval3  32924  dp3mul10  32928  dpadd2  32940  dpmul4  32944  ccatws1f1o  32982  xrslt  33038  xrsclat  33042  xrge0tsmsd  33104  cycpmco2lem7  33163  cycpmconjv  33173  cycpmrn  33174  conjga  33201  elrgspnsubrunlem2  33279  rndrhmcl  33327  fracf1  33338  xrge0slmod  33378  lsmsnorb2  33422  qusbas2  33436  1arithidomlem2  33566  zringfrac  33584  mplvrpmga  33659  mplvrpmmhm  33660  mplvrpmrhm  33661  vieta  33685  rlmdim  33715  rgmoddimOLD  33716  isconstr  33842  iconstr  33872  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  circtopn  33943  tpr2rico  34018  xrge0mulc1cn  34047  lmxrge0  34058  esumpfinvallem  34180  esumcocn  34186  hasheuni  34191  esumcvg  34192  rossros  34286  measinblem  34326  aean  34350  sxbrsigalem3  34378  dya2iocival  34379  dya2iocucvr  34390  sxbrsigalem1  34391  sxbrsigalem2  34392  sxbrsigalem5  34394  sxbrsiga  34396  fiunelcarsg  34422  eulerpartlem1  34473  eulerpartgbij  34478  fibp1  34507  coinfliplem  34585  coinflipprob  34586  ballotlemfval  34596  ballotth  34644  plymulx  34654  circlemethhgt  34749  hgt750lem2  34758  bnj1400  34940  bnj66  34965  bnj882  35031  lfuhgr  35261  derang0  35312  subfacp1lem1  35322  subfacp1lem6  35328  kur14lem7  35355  cvmsss2  35417  cvmliftlem8  35435  cvmliftlem10  35437  satfv1lem  35505  msubfval  35667  quad3  35813  bcprod  35881  bccolsum  35882  faclim  35889  pprodcnveq  36024  dfon4  36034  fobigcup  36041  dfiota3  36064  dfrecs2  36093  dfrdg4  36094  dfint3  36095  rankeq1o  36314  refssfne  36501  ssoninhaus  36591  onint1  36592  bj-rababw  37025  bj-inrab3  37073  bj-imdiridlem  37329  dissneq  37485  dffinxpf  37529  finxpreclem4  37538  rabiun  37733  ptrest  37759  poimirlem3  37763  poimirlem4  37764  poimirlem13  37773  poimirlem16  37776  poimirlem22  37782  poimirlem26  37786  poimirlem27  37787  poimirlem30  37790  cnambfre  37808  ftc1anclem8  37840  fnopabco  37863  abrexdom  37870  cncfres  37905  scottexf  38308  scott0f  38309  inres2  38382  dfres4  38431  dmxrn  38511  xrnres  38549  xrnres2  38550  dfsucmap2  38577  dfcoss2  38615  dfcoss4  38617  1cossres  38631  dmcoss2  38656  1cosscnvxrn  38677  dfeqvrels2  38784  dfcoeleqvrels  38817  redundss3  38824  dffunsALTV5  38885  cdleme3d  40430  cdleme7a  40442  cdleme31sdnN  40586  cdlemk45  41146  420gcd8e4  42199  lcmeprodgcdi  42200  60lcm7e420  42203  420lcm8e840  42204  3lexlogpow5ineq1  42247  3lexlogpow2ineq1  42251  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  aks4d1p1  42269  posbezout  42293  aks6d1c1p4  42304  aks6d1c3  42316  2ap1caineq  42338  sticksstones7  42345  sticksstones12a  42350  sticksstones12  42351  aks6d1c6lem4  42366  imaopab  42429  fmpocos  42432  dfqs2  42435  dfqs3  42436  decaddcom  42481  sumcubes  42510  redvmptabs  42557  readvrec  42559  readvcot  42561  sn-00idlem2  42596  reixi  42620  sum9cubes  42857  mapfzcons  42900  eldioph4b  42995  diophren  42997  pwssplit4  43273  pwfi2f1o  43280  frlmpwfi  43282  mendplusgfval  43365  mendmulrfval  43367  mendvscafval  43370  idomodle  43375  cytpval  43386  arearect  43399  onov0suclim  43458  omabs2  43516  tr3dom  43711  har2o  43729  alephiso2  43741  alephiso3  43742  relintab  43766  dfid7  43795  cnvrcl0  43808  dfrtrcl5  43812  dfrcl3  43858  dfrcl4  43859  comptiunov2i  43889  corcltrcl  43922  neicvgnvo  44298  inductionexd  44338  mnuprdlem2  44456  nznngen  44499  hashnzfz2  44504  lhe4.4ex1a  44512  dvradcnv2  44530  binomcxplemrat  44533  binomcxplemnotnn0  44539  nregmodelf1o  45198  refsum2cnlem1  45224  fiiuncl  45252  iccdifprioo  45704  lptre2pt  45826  limclner  45837  stoweidlem13  46199  stoweidlem32  46218  stoweidlem62  46248  wallispi2lem2  46258  stirlinglem14  46273  dirkertrigeqlem1  46284  dirkercncflem4  46292  fourierdlem42  46335  fourierdlem73  46365  fourierdlem81  46373  fourierdlem92  46384  fourierdlem103  46395  fourierdlem104  46396  fouriercnp  46412  fouriersw  46417  sge0tsms  46566  sge0iunmptlemfi  46599  ovolval5lem3  46840  cnfsmf  46926  nthrucw  47072  lamberte  47076  rnfdmpr  47469  fvmptrabdm  47481  fundcmpsurinjlem1  47586  m11nprm  47789  opoeALTV  47871  nfermltl8rev  47930  sbgoldbo  47975  evengpop3  47986  clnbgrcl  48009  clnbgrnvtx0  48015  usgrexmpl2edg  48217  usgrexmpl2nb0  48219  usgrexmpl2nb3  48222  gpg5order  48248  gpgprismgr4cycllem6  48288  cznabel  48448  cznrng  48449  mpomptx2  48523  2sphere  48937  itscnhlinecirc02plem3  48972  inlinecirc02p  48975  dftpos5  49061  tposresg  49065  icccldii  49106  dfnrm2  49119  dfnrm3  49120  elxpcbasex1ALT  49436  elxpcbasex2ALT  49438  dfswapf2  49448  swapf1a  49456  swapf1f1o  49462  swapf2f1oa  49464  swapfida  49467  setc1oterm  49678  setc1ohomfval  49680  setc1ocofval  49681  funcsetc1o  49684  dfinito4  49688  setc1onsubc  49789  islmd  49852  iscmd  49853  initocmd  49856  termolmd  49857  amgmlemALT  49990