Theorem eqtr4i 2791

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  3eqtr2i  2794  3eqtr2ri  2795  3eqtr4i  2798  3eqtr4ri  2799  rabab  3487  cbvralcsf  3896  cbvrabcsf  3899  dfin5  3914  dfdif2  3915  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  4454  dfif3  4504  dfif5  4506  rabsnif  4691  tpidm  4726  ssunpr  4801  sstp  4803  opidg  4859  dfint2  4916  iunrab  5019  uniiun  5025  intiin  5026  iunid  5027  0iin  5030  uniin1  5041  uniin2  5042  mptv  5219  dfepfr  5647  epfrc  5648  xpundi  5732  xpundir  5733  csbcnv  5874  csbcnvOLD  5875  resiun2  6001  resopab  6038  mptresid  6055  dffr3  6103  dfse2  6104  cnvun  6141  imaundir  6150  imainrect  6181  cnvcnv2  6193  cnvrescnv  6196  cnvcnvres  6208  dmtpop  6221  rnsnopg  6224  resdifdi  6239  rnco2  6257  dmco  6258  co01  6265  unidmrn  6284  dfdm2  6286  predidm  6331  dfmpt3  6673  mptun  6685  funcocnv2  6850  dffv2  6980  fnasrn  7147  fpr  7157  fmptap  7174  rnmptc  7212  riotav  7381  dmoprab  7522  rnoprab2  7525  mpov  7531  mpomptx  7532  abrexex2g  7967  1stval2  8009  2ndval2  8010  fo1st  8012  fo2nd  8013  xp2  8029  dfoprab4f  8059  offval22  8089  fmpoco  8096  fimaproj  8137  tposmpo  8265  tposconst  8266  recsfval  8373  rdgsucmpt2  8423  frsucmpt2  8433  df2o3  8467  o1p1e2  8531  o2p2e4  8532  oarec  8553  omopthlem2  8652  dfqs2  8707  ecqs  8783  qliftf  8809  erovlem  8817  fset0  8857  mapsnf1o3  8899  ixp0x  8930  omf1o  9075  xpf1o  9134  mapunen  9141  enp1ilem  9245  marypha1lem  9400  marypha2lem4  9405  dfoi  9480  infeq5i  9612  oemapso  9658  cantnflem1  9665  rankelop  9853  leweon  10011  r0weon  10012  kmlem11  10160  dju1dif  10172  ackbij1lem16  10233  cf0  10249  cfsmolem  10269  alephsuc3  10582  fpwwe  10648  canthp1lem1  10654  wuncval2  10749  prlem936  11049  m1p1sr  11094  m1m1sr  11095  dfcnqs  11144  ssxr  11296  mul02lem2  11404  addrid  11407  2p2e4  12392  3p2e5  12408  3p3e6  12409  4p2e6  12410  4p3e7  12411  4p4e8  12412  5p2e7  12413  5p3e8  12414  5p4e9  12415  6p2e8  12416  6p3e9  12417  7p2e9  12418  nnzrab  12639  nn0zrab  12640  dec0u  12755  dec0h  12756  decsuc  12765  decsucc  12775  numma  12778  decma  12785  decmac  12786  decma2c  12787  decadd  12788  decaddc  12789  decmul1c  12799  decmul2c  12800  5p5e10  12805  6p4e10  12806  7p3e10  12809  8p2e10  12814  5t5e25  12837  6t6e36  12842  8t6e48  12853  nn0uz  12918  nnuz  12919  xaddcom  13284  x2times  13343  ioomax  13467  iccmax  13468  ioopos  13469  ioorp  13470  prunioo  13526  fseq1p1m1  13645  fzo13pr  13797  fzo0to2pr  13798  fzo0to3tp  13800  om2uzrdg  14012  fzennn  14024  irec  14257  sq10e99m1  14321  facnn  14331  fac0  14332  faclbnd2  14347  faclbnd4lem1  14349  hashfun  14494  hashbclem  14509  hashf1lem1  14512  hashf1lem2  14513  fz1isolem  14518  swrdccatin1  14786  swrdccat3blem  14800  s1co  14896  s2eq2s1eq  14999  s3eqs2s1eq  15001  ofs2  15034  dfid5  15090  dfid6  15091  sgnneg  15163  fsumrev2  15858  fsumparts  15883  fsumiun  15898  isumnn0nn  15921  harmonic  15938  fprod2d  16060  bpoly2  16135  bpoly3  16136  bpoly4  16137  ege2le3  16168  cos1bnd  16267  efieq1re  16279  eirrlem  16284  qnnen  16293  cpnnen  16309  ruclem6  16315  3dvds  16413  pwp1fsum  16473  m1bits  16522  nn0expgcd  16646  algrp1  16656  phiprmpw  16859  prmreclem4  17003  4sqlem11  17039  4sqlem19  17047  dec5dvds  17148  decsplit1  17165  5prm  17192  7prm  17194  1259lem2  17216  1259lem3  17217  1259lem4  17218  1259lem5  17219  1259prm  17220  2503lem1  17221  2503lem2  17222  2503lem3  17223  2503prm  17224  4001lem1  17225  4001lem2  17226  4001lem3  17227  4001lem4  17228  4001prm  17229  strle1  17242  grpbasex  17369  grpplusgx  17370  quslem  17621  xpsrnbas  17649  acsfn1  17741  acsfn2  17743  comfffval2  17781  dfinito2  18084  dftermo2  18085  xpchomfval  18259  xpccofval  18262  1stfval  18271  2ndfval  18274  oduleg  18370  chnub  18702  ismgmid  18750  efmndbas  18969  smndex2dnrinv  19016  degenmgmbas  19037  degenmgm2opdm  19040  grpinvfvi  19095  gaorb  19423  elcntr  19446  cntri  19448  cntrsubgnsg  19459  cntrnsg  19460  setsplusg  19466  oppgcntr  19481  gsumwrev  19482  symgressbas  19498  symgplusg  19499  symgvalstruct  19513  symgga  19523  cayleylem1  19528  psgnunilem2  19611  efgval2  19840  efgredlemc  19861  efgcpbllema  19870  frgpnabllem1  19989  gsumzaddlem  20037  gsumle  20261  opprlem  20472  oppr0  20479  opprneg  20481  rmodislmod  21103  rlmscaf  21380  xrsds  21612  gsumfsum  21636  zringunit  21668  pzriprng1  21700  cnmsgngrp  21781  psgnfix2  21801  relt  21817  ocv0  21879  thlle  21899  thlleval  21900  dsmmval2  21938  frlmip  21980  mplbas  22191  mplplusg  22208  mplmulr  22209  mplvsca2  22215  ressmplbas2  22229  ltbwe  22247  evlslem4  22279  psdmul  22381  psr1bas2  22402  ply1bas  22407  ply1assa  22411  psr1plusg  22432  psr1vsca  22433  psr1mulr  22434  ply1plusg  22435  ply1vsca  22436  ply1mulr  22437  ply1mpl0  22468  ply1mpl1  22470  coe1mul  22483  matgsum  22646  smadiadetglem1  22880  indistpsx  23219  iuncld  23254  tgrest  23368  resstopn  23395  leordtval2  23421  xkouni  23809  ptclsg  23825  ptuncnv  24017  ptunhmeo  24018  alexsubALTlem4  24260  tsmsf1o  24355  ucnimalem  24489  ressxms  24735  uniretop  24972  cnfldtopn  24991  xrtgioo  25017  zcld  25024  icccmp  25036  xrge0gsumle  25044  xrge0tsms  25045  metnrmlem3  25072  fsum2cn  25083  cnmpopc  25140  oprpiece1res1  25163  oprpiece1res2  25164  evth  25171  evth2  25172  om1opn  25248  pi1xfrf  25265  pi1xfrcnv  25269  pi1cof  25271  clsocv  25462  cncmet  25534  cnflduss  25568  rrxprds  25601  ehlbase  25627  ismbl  25738  shftmbl  25750  ioorinv  25788  itg1addlem4  25911  itg2cnlem1  25973  itg0  25992  itgss3  26027  ditgneg  26069  limcdif  26088  limciun  26106  dvexp  26165  dvef  26192  dvcnvrelem2  26230  ftc1  26254  plymulidp  26496  aannenlem2  26545  dvradcnv  26637  pserdvlem2  26644  reefgim  26666  cospi  26690  sincos6thpi  26734  tanregt0  26757  dflog2  26778  logfac  26819  dvlog  26869  cxpexp  26886  cxpmul2  26907  cxpsqrt  26921  dvsqrt  26960  dvcnsqrt  26962  cxpcn2  26964  isosctrlem2  27037  1cubrlem  27059  1cubr  27060  quart1lem  27073  atancj  27128  atanlogaddlem  27131  atansopn  27150  leibpilem2  27159  log2cnv  27162  log2ublem3  27166  birthdaylem1  27169  birthdaylem2  27170  birthday  27172  dfarea  27178  lgamgulmlem5  27250  lgambdd  27254  ftalem3  27292  basellem2  27299  ppiprm  27368  ppinprm  27369  chtprm  27370  chtnprm  27371  ppi2  27387  ppi3  27388  ppiub  27421  chtub  27429  bclbnd  27497  bposlem8  27508  lgsdilem  27541  lgsdir2lem2  27543  lgsquadlem2  27598  lgsquad2lem2  27602  2lgsoddprmlem3c  27629  rplogsum  27744  mulog2sumlem2  27752  pnt2  27830  bdayfo  27894  bday0  28057  bday1  28060  old1  28111  addsasslem2  28250  negbdaylem  28302  muls01  28358  abssnid  28489  1p1e2s  28662  n0seo  28667  twocut  28669  halfcut  28704  pw2cutp1  28707  pw2cut2  28708  istrkg2ld  28782  axsegconlem9  29332  ax5seglem7  29342  iedgedg  29457  lfuhgr  29555  uspgrf1oedg  29583  nbgrcl  29745  nbgrnvtx0  29749  rusgrprc  30000  pthsfval  30133  wlkiswwlks2lem4  30290  wlkiswwlks2lem5  30291  clwwlkvbij  30533  konigsbergumgr  30675  ex-pw  30853  ex-xp  30860  ex-rn  30864  nvvop  31034  nvm  31066  cnims  31118  ip0i  31250  ip1ilem  31251  ipdirilem  31254  ipasslem10  31264  h2hva  31399  h2hsm  31400  h2hvs  31402  axhfvadd-zf  31407  axhvcom-zf  31408  axhvass-zf  31409  axhv0cl-zf  31410  axhvaddid-zf  31411  axhfvmul-zf  31412  axhvmulid-zf  31413  axhvmulass-zf  31414  axhvdistr1-zf  31415  axhvdistr2-zf  31416  axhvmul0-zf  31417  axhfi-zf  31418  axhis1-zf  31419  axhis2-zf  31420  axhis3-zf  31421  axhis4-zf  31422  axhcompl-zf  31423  normlem0  31534  normlem1  31535  normlem2  31536  normlem4  31538  normlem9  31543  bcseqi  31545  dfhnorm2  31547  norm3difi  31572  normpari  31579  normpar2i  31581  polid2i  31582  polidi  31583  hhba  31592  hhims  31597  hhims2  31598  hhsssh  31694  hhssims  31699  hhssims2  31700  shsval3i  31813  dfch2  31832  cmcm2i  32018  fh2  32044  qlaxr3i  32061  spansnji  32071  pjcji  32109  ho0val  32175  df0op2  32177  hosd1i  32247  hosd2i  32248  eigorthi  32262  hhlnoi  32325  hhnmoi  32326  hhbloi  32327  bra0  32375  nmop0  32411  nmfn0  32412  lnopeq0lem1  32430  lnopunilem1  32435  lnophmlem2  32442  nmopcoadji  32526  pjhmopidm  32608  cvmdi  32749  cdj3lem3  32863  cdj3lem3b  32865  abrexdomjm  32926  iundifdifd  32979  iundifdif  32980  mpomptxf  33096  df1stres  33122  df2ndres  33123  intimafv  33129  fcobijfs  33138  fcobijfs2  33139  resf1o  33147  fpwrelmapffslem  33149  dpval3  33285  dp3mul10  33289  dpadd2  33301  dpmul4  33305  ccatws1f1o  33339  xrslt  33393  xrsclat  33397  xrge0tsmsd  33459  cycpmco2lem7  33518  cycpmconjv  33528  cycpmrn  33529  conjga  33556  elrgspnsubrunlem2  33634  rndrhmcl  33683  fracf1  33694  xrge0slmod  33734  lsmsnorb2  33771  qusbas2  33781  1arithidomlem2  33892  zringfrac  33910  selvply1rhm0  33982  mplvrpmga  34001  mplvrpmmhm  34002  mplvrpmrhm  34003  psrmonprod  34008  mplmonprod  34010  vieta  34036  rlmdim  34066  isconstr  34192  iconstr  34222  cos9thpiminplylem4  34241  cos9thpiminplylem5  34242  circtopn  34293  tpr2rico  34368  xrge0mulc1cn  34397  lmxrge0  34408  esumpfinvallem  34530  esumcocn  34536  hasheuni  34541  esumcvg  34542  rossros  34637  measinblem  34677  aean  34701  sxbrsigalem3  34729  dya2iocival  34730  dya2iocucvr  34741  sxbrsigalem1  34742  sxbrsigalem2  34743  sxbrsigalem5  34745  sxbrsiga  34747  fiunelcarsg  34773  eulerpartlem1  34824  eulerpartgbij  34829  fibp1  34858  coinfliplem  34936  coinflipprob  34937  ballotlemfval  34947  ballotth  34995  circlemethhgt  35097  hgt750lem2  35106  bnj1400  35290  bnj66  35315  bnj882  35381  dfscott2  35571  dfscott3  35572  derang0  35700  subfacp1lem1  35710  subfacp1lem6  35716  kur14lem7  35743  cvmsss2  35805  cvmliftlem8  35823  cvmliftlem10  35825  satfv1lem  35893  msubfval  36055  quad3  36201  bcprod  36269  bccolsum  36270  faclim  36277  pprodcnveq  36412  dfon4  36422  fobigcup  36429  dfiota3  36452  dfrecs2  36481  dfrdg4  36482  dfint3  36483  rankeq1o  36702  refssfne  36928  ssoninhaus  37018  onint1  37019  ttciun  37084  bj-dfnul2  37222  bj-rababw  37575  bj-inrab3  37624  bj-imdiridlem  37888  dissneq  38046  dffinxpf  38090  finxpreclem4  38099  rabiun  38303  ptrest  38329  poimirlem3  38333  poimirlem4  38334  poimirlem13  38343  poimirlem16  38346  poimirlem22  38352  poimirlem26  38356  poimirlem27  38357  poimirlem30  38360  cnambfre  38378  ftc1anclem8  38410  fnopabco  38434  abrexdom  38441  cncfres  38476  scottexf  38877  scott0f  38878  inres2  38956  eqrabi  38965  xpv  38971  dfres4  39008  dmxrn  39096  xrnres  39134  xrnres2  39135  rnqmap  39163  dfsucmap2  39173  dfcoss2  39212  dfcoss4  39214  1cossres  39228  dmcoss2  39253  1cosscnvxrn  39274  dfeqvrels2  39381  dfcoeleqvrels  39414  redundss3  39421  dffunsALTV5  39481  dfpeters2  39683  cdleme3d  41065  cdleme7a  41077  cdleme31sdnN  41221  cdlemk45  41781  420gcd8e4  42833  lcmeprodgcdi  42834  60lcm7e420  42837  420lcm8e840  42838  3lexlogpow5ineq1  42881  3lexlogpow2ineq1  42885  3lexlogpow2ineq2  42886  3lexlogpow5ineq5  42887  aks4d1p1  42903  posbezout  42927  aks6d1c1p4  42938  aks6d1c3  42950  2ap1caineq  42972  sticksstones7  42979  sticksstones12a  42984  sticksstones12  42985  aks6d1c6lem4  43000  25or6to4  43033  imaopab  43062  fmpocos  43064  dfqs3  43067  decaddcom  43105  sumcubes  43134  redvmptabs  43181  readvrec  43183  readvcot  43185  sn-00idlem2  43220  reixi  43244  sum9cubes  43464  mapfzcons  43507  eldioph4b  43598  diophren  43600  pwssplit4  43876  pwfi2f1o  43883  frlmpwfi  43885  mendplusgfval  43968  mendmulrfval  43970  mendvscafval  43973  idomodle  43978  cytpval  43989  arearect  44002  onov0suclim  44061  omabs2  44119  tr3dom  44314  har2o  44332  alephiso2  44344  alephiso3  44345  relintab  44369  dfid7  44398  cnvrcl0  44411  dfrtrcl5  44415  dfrcl3  44461  dfrcl4  44462  comptiunov2i  44492  corcltrcl  44525  neicvgnvo  44901  inductionexd  44941  mnuprdlem2  45043  nznngen  45086  hashnzfz2  45091  lhe4.4ex1a  45099  dvradcnv2  45117  binomcxplemrat  45120  binomcxplemnotnn0  45126  nregmodelf1o  45784  refsum2cnlem1  45817  fiiuncl  45845  iccdifprioo  46292  lptre2pt  46414  limclner  46425  stoweidlem13  46787  stoweidlem32  46806  stoweidlem62  46836  wallispi2lem2  46846  stirlinglem14  46861  dirkertrigeqlem1  46872  dirkercncflem4  46880  fourierdlem42  46923  fourierdlem73  46953  fourierdlem81  46961  fourierdlem92  46972  fourierdlem103  46983  fourierdlem104  46984  fouriercnp  47000  fouriersw  47005  sge0tsms  47154  sge0iunmptlemfi  47187  ovolval5lem3  47428  cnfsmf  47514  lamberte  47685  rnfdmpr  48078  fvmptrabdm  48090  fundcmpsurinjlem1  48207  m11nprm  48413  ppi1sum  48443  opoeALTV  48508  nfermltl8rev  48567  sbgoldbo  48612  evengpop3  48623  clnbgrcl  48646  clnbgrnvtx0  48652  usgrexmpl2edg  48854  usgrexmpl2nb0  48856  usgrexmpl2nb3  48859  gpg5order  48885  gpgprismgr4cycllem6  48925  cznabel  49084  cznrng  49085  mpomptx2  49174  2sphere  49588  itscnhlinecirc02plem3  49623  inlinecirc02p  49626  dftpos5  49711  tposresg  49715  icccldii  49756  dfnrm2  49769  dfnrm3  49770  elxpcbasex1ALT  50086  elxpcbasex2ALT  50088  dfswapf2  50098  swapf1a  50106  swapf1f1o  50112  swapf2f1oa  50114  swapfida  50117  setc1oterm  50328  setc1ohomfval  50330  setc1ocofval  50331  funcsetc1o  50334  dfinito4  50338  setc1onsubc  50439  islmd  50502  iscmd  50503  initocmd  50506  termolmd  50507  amgmlemALT  50710