Theorem eqtr4i 2824

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

Syntax hints:   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  3eqtr2i  2827  3eqtr2ri  2828  3eqtr4i  2831  3eqtr4ri  2832  rabab  3470  cbvralcsf  3870  cbvrabcsf  3873  dfin5  3889  dfdif2  3890  uneqin  4205  unrab  4226  inrab  4227  inrab2  4228  difrab  4229  dfrab3ss  4233  rabun2  4234  difidALT  4285  rabxm  4294  elnelun  4297  abf  4310  difdifdir  4395  dfif3  4439  dfif5  4441  rabsnif  4619  tpidm  4654  ssunpr  4725  sstp  4727  opidg  4784  dfint2  4840  iunrab  4939  uniiun  4945  intiin  4946  0iin  4950  mptv  5135  dfepfr  5504  epfrc  5505  xpundi  5584  xpundir  5585  csbcnv  5718  resiun2  5839  resopab  5869  mptresid  5885  opabresidOLD  5886  dffr3  5929  dfse2  5930  cnvun  5968  imaundir  5976  imainrect  6005  cnvcnv2  6017  cnvrescnv  6019  cnvcnvres  6029  dmtpop  6042  rnsnopg  6045  rnco2  6073  dmco  6074  co01  6081  unidmrn  6098  dfdm2  6100  predidm  6138  tz6.26  6147  dfmpt3  6454  mptun  6466  funcocnv2  6614  dffv2  6733  fnasrn  6884  fpr  6893  fmptap  6909  rnmptc  6946  rnmptcOLD  6947  riotav  7098  dmoprab  7234  rnoprab2  7237  mpov  7243  mpomptx  7244  abrexex2g  7647  1stval2  7688  2ndval2  7689  fo1st  7691  fo2nd  7692  xp2  7708  dfoprab4f  7736  offval22  7766  fmpoco  7773  fimaproj  7812  tposmpo  7912  tposconst  7913  recsfval  8000  rdgsucmpt2  8049  frsucmpt2w  8058  frsucmpt2  8059  df2o3  8100  o1p1e2  8148  o2p2e4  8149  o2p2e4OLD  8150  oarec  8171  omopthlem2  8266  ecqs  8344  qliftf  8368  erovlem  8376  mapsnf1o3  8442  ixp0x  8473  omf1o  8603  xpf1o  8663  mapunen  8670  enp1ilem  8736  pwfi  8803  marypha1lem  8881  marypha2lem4  8886  dfoi  8959  infeq5i  9083  oemapso  9129  cantnflem1  9136  rankelop  9287  leweon  9422  r0weon  9423  kmlem11  9571  dju1dif  9583  ackbij1lem16  9646  cf0  9662  cfsmolem  9681  alephsuc3  9991  fpwwe  10057  canthp1lem1  10063  wuncval2  10158  prlem936  10458  m1p1sr  10503  m1m1sr  10504  dfcnqs  10553  ssxr  10699  mul02lem2  10806  addid1  10809  2p2e4  11760  3p2e5  11776  3p3e6  11777  4p2e6  11778  4p3e7  11779  4p4e8  11780  5p2e7  11781  5p3e8  11782  5p4e9  11783  6p2e8  11784  6p3e9  11785  7p2e9  11786  nnzrab  11998  nn0zrab  11999  dec0u  12107  dec0h  12108  decsuc  12117  decsucc  12127  numma  12130  decma  12137  decmac  12138  decma2c  12139  decadd  12140  decaddc  12141  decmul1c  12151  decmul2c  12152  5p5e10  12157  6p4e10  12158  7p3e10  12161  8p2e10  12166  5t5e25  12189  6t6e36  12194  8t6e48  12205  nn0uz  12268  nnuz  12269  xaddcom  12621  x2times  12680  ioomax  12800  iccmax  12801  ioopos  12802  ioorp  12803  prunioo  12859  fseq1p1m1  12976  fzo13pr  13116  fzo0to2pr  13117  fzo0to3tp  13118  om2uzrdg  13319  fzennn  13331  irec  13560  sq10e99m1  13621  facnn  13631  fac0  13632  faclbnd2  13647  faclbnd4lem1  13649  hashfun  13794  hashbclem  13806  hashf1lem1  13809  hashf1lem2  13810  fz1isolem  13815  swrdccatin1  14078  swrdccat3blem  14092  s1co  14186  s2eq2s1eq  14289  s3eqs2s1eq  14291  ofs2  14322  dfid5  14378  dfid6  14379  fsumrev2  15129  fsumparts  15153  fsumiun  15168  isumnn0nn  15189  harmonic  15206  fprod2d  15327  bpoly2  15403  bpoly3  15404  bpoly4  15405  ege2le3  15435  cos1bnd  15532  efieq1re  15544  eirrlem  15549  qnnen  15558  cpnnen  15574  ruclem6  15580  3dvds  15672  pwp1fsum  15732  m1bits  15779  algrp1  15908  phiprmpw  16103  prmreclem4  16245  4sqlem11  16281  4sqlem19  16289  dec5dvds  16390  decsplit1  16408  5prm  16434  7prm  16436  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  strle1  16584  grpbasex  16605  grpplusgx  16606  quslem  16808  xpsrnbas  16836  acsfn1  16924  acsfn2  16926  comfffval2  16963  xpchomfval  17421  xpccofval  17424  1stfval  17433  2ndfval  17436  oduleg  17734  ismgmid  17867  efmndbas  18028  smndex2dnrinv  18072  grpinvfvi  18138  gaorb  18429  cntri  18453  cntrsubgnsg  18463  cntrnsg  18464  oppglem  18470  oppgcntr  18485  gsumwrev  18486  symgressbas  18502  symgplusg  18503  symgvalstruct  18517  symgga  18527  cayleylem1  18532  psgnunilem2  18615  efgval2  18842  efgredlemc  18863  efgcpbllema  18872  frgpnabllem1  18986  gsumzaddlem  19034  mgplem  19237  opprlem  19374  oppr0  19379  opprneg  19381  rmodislmod  19695  rlmscaf  19974  xrsds  20134  gsumfsum  20158  zringunit  20181  cnmsgngrp  20268  psgnfix2  20288  relt  20304  ocv0  20366  thlle  20386  thlleval  20387  dsmmval2  20425  frlmip  20467  mplbas  20667  mpladd  20680  mplmul  20682  mplvsca2  20685  ressmplbas2  20695  ltbwe  20712  evlslem4  20747  psr1bas2  20819  ply1bas  20824  ply1assa  20828  mplplusg  20849  mplmulr  20850  psr1plusg  20851  psr1vsca  20852  psr1mulr  20853  ply1plusg  20854  ply1vsca  20855  ply1mulr  20856  ply1mpl0  20884  ply1mpl1  20886  coe1mul  20899  matgsum  21042  smadiadetglem1  21276  indistpsx  21615  iuncld  21650  tgrest  21764  resstopn  21791  leordtval2  21817  xkouni  22204  ptclsg  22220  ptuncnv  22412  ptunhmeo  22413  alexsubALTlem4  22655  tsmsf1o  22750  ucnimalem  22886  ressxms  23132  uniretop  23368  cnfldtopn  23387  xrtgioo  23411  zcld  23418  icccmp  23430  xrge0gsumle  23438  xrge0tsms  23439  metnrmlem3  23466  fsum2cn  23476  cnmpopc  23533  oprpiece1res1  23556  oprpiece1res2  23557  evth  23564  evth2  23565  om1opn  23641  pi1xfrf  23658  pi1xfrcnv  23662  pi1cof  23664  clsocv  23854  cncmet  23926  cnflduss  23960  rrxprds  23993  ehlbase  24019  ismbl  24130  shftmbl  24142  ioorinv  24180  itg1addlem4  24303  itg2cnlem1  24365  itg0  24383  itgss3  24418  ditgneg  24460  limcdif  24479  limciun  24497  dvexp  24556  dvef  24583  dvcnvrelem2  24621  ftc1  24645  aannenlem2  24925  dvradcnv  25016  pserdvlem2  25023  reefgim  25045  cospi  25065  sincos6thpi  25108  tanregt0  25131  dflog2  25152  logfac  25192  dvlog  25242  cxpexp  25259  cxpmul2  25280  cxpsqrt  25294  dvsqrt  25331  dvcnsqrt  25333  cxpcn2  25335  isosctrlem2  25405  1cubrlem  25427  1cubr  25428  quart1lem  25441  atancj  25496  atanlogaddlem  25499  atansopn  25518  leibpilem2  25527  log2cnv  25530  log2ublem3  25534  birthdaylem1  25537  birthdaylem2  25538  birthday  25540  dfarea  25546  lgamgulmlem5  25618  lgambdd  25622  ftalem3  25660  basellem2  25667  ppiprm  25736  ppinprm  25737  chtprm  25738  chtnprm  25739  ppi2  25755  ppi3  25756  ppiub  25788  chtub  25796  bclbnd  25864  bposlem8  25875  lgsdilem  25908  lgsdir2lem2  25910  lgsquadlem2  25965  lgsquad2lem2  25969  2lgsoddprmlem3c  25996  rplogsum  26111  mulog2sumlem2  26119  pnt2  26197  istrkg2ld  26254  axsegconlem9  26719  ax5seglem7  26729  iedgedg  26843  uspgrf1oedg  26966  nbgrcl  27125  nbgrnvtx0  27129  rusgrprc  27380  wlkiswwlks2lem4  27658  wlkiswwlks2lem5  27659  clwwlkvbij  27898  konigsbergumgr  28036  ex-pw  28214  ex-xp  28221  ex-rn  28225  nvvop  28392  nvm  28424  cnims  28476  ip0i  28608  ip1ilem  28609  ipdirilem  28612  ipasslem10  28622  h2hva  28757  h2hsm  28758  h2hvs  28760  axhfvadd-zf  28765  axhvcom-zf  28766  axhvass-zf  28767  axhv0cl-zf  28768  axhvaddid-zf  28769  axhfvmul-zf  28770  axhvmulid-zf  28771  axhvmulass-zf  28772  axhvdistr1-zf  28773  axhvdistr2-zf  28774  axhvmul0-zf  28775  axhfi-zf  28776  axhis1-zf  28777  axhis2-zf  28778  axhis3-zf  28779  axhis4-zf  28780  axhcompl-zf  28781  normlem0  28892  normlem1  28893  normlem2  28894  normlem4  28896  normlem9  28901  bcseqi  28903  dfhnorm2  28905  norm3difi  28930  normpari  28937  normpar2i  28939  polid2i  28940  polidi  28941  hhba  28950  hhims  28955  hhims2  28956  hhsssh  29052  hhssims  29057  hhssims2  29058  shsval3i  29171  dfch2  29190  cmcm2i  29376  fh2  29402  qlaxr3i  29419  spansnji  29429  pjcji  29467  ho0val  29533  df0op2  29535  hosd1i  29605  hosd2i  29606  eigorthi  29620  hhlnoi  29683  hhnmoi  29684  hhbloi  29685  bra0  29733  nmop0  29769  nmfn0  29770  lnopeq0lem1  29788  lnopunilem1  29793  lnophmlem2  29800  nmopcoadji  29884  pjhmopidm  29966  cvmdi  30107  cdj3lem3  30221  cdj3lem3b  30223  abrexdomjm  30275  uniin1  30315  uniin2  30316  iundifdifd  30325  iundifdif  30326  mpomptxf  30442  df1stres  30463  df2ndres  30464  intimafv  30470  fcobijfs  30485  resf1o  30492  fpwrelmapffslem  30494  dpval3  30596  dp3mul10  30600  dpadd2  30612  dpmul4  30616  xrslt  30710  xrsclat  30714  xrge0tsmsd  30742  gsumle  30775  cycpmco2lem7  30824  cycpmconjv  30834  cycpmrn  30835  xrge0slmod  30968  rgmoddim  31096  circtopn  31190  tpr2rico  31265  xrge0mulc1cn  31294  lmxrge0  31305  esumpfinvallem  31443  esumcocn  31449  hasheuni  31454  esumcvg  31455  rossros  31549  measinblem  31589  aean  31613  sxbrsigalem3  31640  dya2iocival  31641  dya2iocucvr  31652  sxbrsigalem1  31653  sxbrsigalem2  31654  sxbrsigalem5  31656  sxbrsiga  31658  fiunelcarsg  31684  eulerpartlem1  31735  eulerpartgbij  31740  fibp1  31769  coinfliplem  31846  coinflipprob  31847  ballotlemfval  31857  ballotth  31905  sgnneg  31908  plymulx  31928  circlemethhgt  32024  hgt750lem2  32033  bnj1400  32217  bnj66  32242  bnj882  32308  lfuhgr  32477  derang0  32529  subfacp1lem1  32539  subfacp1lem6  32545  kur14lem7  32572  cvmsss2  32634  cvmliftlem8  32652  cvmliftlem10  32654  satfv1lem  32722  msubfval  32884  quad3  33026  bcprod  33083  bccolsum  33084  faclim  33091  dftrpred2  33171  bdayfo  33295  pprodcnveq  33457  dfon4  33467  fobigcup  33474  dfiota3  33497  dfrecs2  33524  dfrdg4  33525  dfint3  33526  rankeq1o  33745  refssfne  33819  ssoninhaus  33909  onint1  33910  bj-rababw  34321  bj-inrab3  34371  bj-imdiridlem  34600  dissneq  34758  dffinxpf  34802  finxpreclem4  34811  wl-dfrabsb  35026  rabiun  35030  ptrest  35056  poimirlem3  35060  poimirlem4  35061  poimirlem13  35070  poimirlem16  35073  poimirlem22  35079  poimirlem26  35083  poimirlem27  35084  poimirlem30  35087  cnambfre  35105  ftc1anclem8  35137  fnopabco  35161  abrexdom  35168  cncfres  35203  scottexf  35606  scott0f  35607  inres2  35666  dfres4  35710  xrnres  35810  xrnres2  35811  dfcoss2  35821  dfcoss4  35823  1cossres  35834  dmcoss2  35854  1cosscnvxrn  35875  dfeqvrels2  35983  dfcoeleqvrels  36016  redundss3  36023  dffunsALTV5  36080  cdleme3d  37527  cdleme7a  37539  cdleme31sdnN  37683  cdlemk45  38243  420gcd8e4  39294  lcmeprodgcdi  39295  60lcm7e420  39298  420lcm8e840  39299  3lexlogpow5ineq1  39341  2ap1caineq  39349  imaopab  39413  dfqs2  39417  dfqs3  39418  decaddcom  39478  nn0expgcd  39492  sn-00idlem2  39537  reixi  39559  mapfzcons  39657  eldioph4b  39752  diophren  39754  pwssplit4  40033  pwfi2f1o  40040  frlmpwfi  40042  mendplusgfval  40129  mendmulrfval  40131  mendvscafval  40134  idomodle  40140  cytpval  40153  arearect  40165  tr3dom  40236  alephiso2  40257  alephiso3  40258  relintab  40283  dfid7  40312  cnvrcl0  40325  dfrtrcl5  40329  dfrcl3  40376  dfrcl4  40377  comptiunov2i  40407  corcltrcl  40440  neicvgnvo  40818  inductionexd  40858  mnuprdlem2  40981  nznngen  41020  hashnzfz2  41025  lhe4.4ex1a  41033  dvradcnv2  41051  binomcxplemrat  41054  binomcxplemnotnn0  41060  refsum2cnlem1  41666  fiiuncl  41699  iccdifprioo  42153  lptre2pt  42282  limclner  42293  stoweidlem13  42655  stoweidlem32  42674  stoweidlem62  42704  wallispi2lem2  42714  stirlinglem14  42729  dirkertrigeqlem1  42740  dirkercncflem4  42748  fourierdlem42  42791  fourierdlem73  42821  fourierdlem81  42829  fourierdlem92  42840  fourierdlem103  42851  fourierdlem104  42852  fouriercnp  42868  fouriersw  42873  sge0tsms  43019  sge0iunmptlemfi  43052  ovolval5lem3  43293  cnfsmf  43374  rnfdmpr  43837  fvmptrabdm  43849  fundcmpsurinjlem1  43915  m11nprm  44119  opoeALTV  44201  nfermltl8rev  44260  sbgoldbo  44305  evengpop3  44316  cznabel  44578  cznrng  44579  mpomptx2  44736  2sphere  45163  itscnhlinecirc02plem3  45198  inlinecirc02p  45201  amgmlemALT  45331