Theorem eqtr4i 2847

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

Syntax hints:   = wceq 1537

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 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  3eqtr2i  2850  3eqtr2ri  2851  3eqtr4i  2854  3eqtr4ri  2855  rabab  3523  cbvralcsf  3925  cbvrabcsf  3928  dfin5  3944  dfdif2  3945  uneqin  4255  unrab  4274  inrab  4275  inrab2  4276  difrab  4277  dfrab3ss  4281  rabun2  4282  difidALT  4331  rabxm  4340  elnelun  4343  difdifdir  4437  dfif3  4481  dfif5  4483  rabsnif  4659  tpidm  4694  ssunpr  4765  sstp  4767  opidg  4822  dfint2  4878  iunrab  4976  uniiun  4982  intiin  4983  0iin  4987  mptv  5171  dfepfr  5540  epfrc  5541  xpundi  5620  xpundir  5621  csbcnv  5754  resiun2  5874  resopab  5902  mptresid  5918  opabresidOLD  5919  dffr3  5962  dfse2  5963  cnvun  6001  imaundir  6009  imainrect  6038  cnvcnv2  6050  cnvrescnv  6052  cnvcnvres  6062  dmtpop  6075  rnsnopg  6078  rnco2  6106  dmco  6107  co01  6114  unidmrn  6130  dfdm2  6132  predidm  6170  tz6.26  6179  dfmpt3  6482  mptun  6494  funcocnv2  6639  dffv2  6756  fnasrn  6907  fpr  6916  fmptap  6932  rnmptc  6969  rnmptcOLD  6970  riotav  7119  dmoprab  7255  rnoprab2  7258  mpov  7264  mpomptx  7265  abrexex2g  7665  1stval2  7706  2ndval2  7707  fo1st  7709  fo2nd  7710  xp2  7726  dfoprab4f  7754  offval22  7783  fmpoco  7790  fimaproj  7829  tposmpo  7929  tposconst  7930  recsfval  8017  rdgsucmpt2  8066  frsucmpt2w  8075  frsucmpt2  8076  df2o3  8117  o1p1e2  8165  o2p2e4  8166  o2p2e4OLD  8167  oarec  8188  omopthlem2  8283  ecqs  8361  qliftf  8385  erovlem  8393  mapsnf1o3  8459  ixp0x  8490  omf1o  8620  xpf1o  8679  mapunen  8686  enp1ilem  8752  pwfi  8819  marypha1lem  8897  marypha2lem4  8902  dfoi  8975  infeq5i  9099  oemapso  9145  cantnflem1  9152  rankelop  9303  leweon  9437  r0weon  9438  kmlem11  9586  dju1dif  9598  ackbij1lem16  9657  cf0  9673  cfsmolem  9692  alephsuc3  10002  fpwwe  10068  canthp1lem1  10074  wuncval2  10169  prlem936  10469  m1p1sr  10514  m1m1sr  10515  dfcnqs  10564  ssxr  10710  mul02lem2  10817  addid1  10820  2p2e4  11773  3p2e5  11789  3p3e6  11790  4p2e6  11791  4p3e7  11792  4p4e8  11793  5p2e7  11794  5p3e8  11795  5p4e9  11796  6p2e8  11797  6p3e9  11798  7p2e9  11799  nnzrab  12011  nn0zrab  12012  dec0u  12120  dec0h  12121  decsuc  12130  decsucc  12140  numma  12143  decma  12150  decmac  12151  decma2c  12152  decadd  12153  decaddc  12154  decmul1c  12164  decmul2c  12165  5p5e10  12170  6p4e10  12171  7p3e10  12174  8p2e10  12179  5t5e25  12202  6t6e36  12207  8t6e48  12218  nn0uz  12281  nnuz  12282  xaddcom  12634  x2times  12693  ioomax  12812  iccmax  12813  ioopos  12814  ioorp  12815  prunioo  12868  fseq1p1m1  12982  fzo13pr  13122  fzo0to2pr  13123  fzo0to3tp  13124  om2uzrdg  13325  fzennn  13337  irec  13565  sq10e99m1  13626  facnn  13636  fac0  13637  faclbnd2  13652  faclbnd4lem1  13654  hashfun  13799  hashbclem  13811  hashf1lem1  13814  hashf1lem2  13815  fz1isolem  13820  swrdccatin1  14087  swrdccat3blem  14101  s1co  14195  s2eq2s1eq  14298  s3eqs2s1eq  14300  ofs2  14331  dfid5  14386  dfid6  14387  fsumrev2  15137  fsumparts  15161  fsumiun  15176  isumnn0nn  15197  harmonic  15214  fprod2d  15335  bpoly2  15411  bpoly3  15412  bpoly4  15413  ege2le3  15443  cos1bnd  15540  efieq1re  15552  eirrlem  15557  qnnen  15566  cpnnen  15582  ruclem6  15588  3dvds  15680  pwp1fsum  15742  m1bits  15789  algrp1  15918  phiprmpw  16113  prmreclem4  16255  4sqlem11  16291  4sqlem19  16299  dec5dvds  16400  decsplit1  16418  5prm  16442  7prm  16444  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  strle1  16592  grpbasex  16613  grpplusgx  16614  quslem  16816  xpsrnbas  16844  acsfn1  16932  acsfn2  16934  comfffval2  16971  xpchomfval  17429  xpccofval  17432  1stfval  17441  2ndfval  17444  oduleg  17742  ismgmid  17875  efmndbas  18036  smndex2dnrinv  18080  grpinvfvi  18146  gaorb  18437  cntri  18461  cntrsubgnsg  18471  cntrnsg  18472  oppglem  18478  oppgcntr  18493  gsumwrev  18494  symgressbas  18510  symgplusg  18511  symgvalstruct  18525  symgga  18535  cayleylem1  18540  psgnunilem2  18623  efgval2  18850  efgredlemc  18871  efgcpbllema  18880  frgpnabllem1  18993  gsumzaddlem  19041  mgplem  19244  opprlem  19378  oppr0  19383  opprneg  19385  rmodislmod  19702  rlmscaf  19981  mplbas  20209  mpladd  20222  mplmul  20223  mplvsca2  20226  ressmplbas2  20236  ltbwe  20253  evlslem4  20288  psr1bas2  20358  ply1bas  20363  ply1assa  20367  mplplusg  20388  mplmulr  20389  psr1plusg  20390  psr1vsca  20391  psr1mulr  20392  ply1plusg  20393  ply1vsca  20394  ply1mulr  20395  ply1mpl0  20423  ply1mpl1  20425  coe1mul  20438  xrsds  20588  gsumfsum  20612  zringunit  20635  cnmsgngrp  20723  psgnfix2  20743  relt  20759  ocv0  20821  thlle  20841  thlleval  20842  dsmmval2  20880  frlmip  20922  matgsum  21046  smadiadetglem1  21280  indistpsx  21618  iuncld  21653  tgrest  21767  resstopn  21794  leordtval2  21820  xkouni  22207  ptclsg  22223  ptuncnv  22415  ptunhmeo  22416  alexsubALTlem4  22658  tsmsf1o  22753  ucnimalem  22889  ressxms  23135  uniretop  23371  cnfldtopn  23390  xrtgioo  23414  zcld  23421  icccmp  23433  xrge0gsumle  23441  xrge0tsms  23442  metnrmlem3  23469  fsum2cn  23479  cnmpopc  23532  oprpiece1res1  23555  oprpiece1res2  23556  evth  23563  evth2  23564  om1opn  23640  pi1xfrf  23657  pi1xfrcnv  23661  pi1cof  23663  clsocv  23853  cncmet  23925  cnflduss  23959  rrxprds  23992  ehlbase  24018  ismbl  24127  shftmbl  24139  ioorinv  24177  itg1addlem4  24300  itg2cnlem1  24362  itg0  24380  itgss3  24415  ditgneg  24455  limcdif  24474  limciun  24492  dvexp  24550  dvef  24577  dvcnvrelem2  24615  ftc1  24639  aannenlem2  24918  dvradcnv  25009  pserdvlem2  25016  reefgim  25038  cospi  25058  sincos6thpi  25101  tanregt0  25123  dflog2  25144  logfac  25184  dvlog  25234  cxpexp  25251  cxpmul2  25272  cxpsqrt  25286  dvsqrt  25323  dvcnsqrt  25325  cxpcn2  25327  isosctrlem2  25397  1cubrlem  25419  1cubr  25420  quart1lem  25433  atancj  25488  atanlogaddlem  25491  atansopn  25510  leibpilem2  25519  log2cnv  25522  log2ublem3  25526  birthdaylem1  25529  birthdaylem2  25530  birthday  25532  dfarea  25538  lgamgulmlem5  25610  lgambdd  25614  ftalem3  25652  basellem2  25659  ppiprm  25728  ppinprm  25729  chtprm  25730  chtnprm  25731  ppi2  25747  ppi3  25748  ppiub  25780  chtub  25788  bclbnd  25856  bposlem8  25867  lgsdilem  25900  lgsdir2lem2  25902  lgsquadlem2  25957  lgsquad2lem2  25961  2lgsoddprmlem3c  25988  rplogsum  26103  mulog2sumlem2  26111  pnt2  26189  istrkg2ld  26246  axsegconlem9  26711  ax5seglem7  26721  iedgedg  26835  uspgrf1oedg  26958  nbgrcl  27117  nbgrnvtx0  27121  rusgrprc  27372  wlkiswwlks2lem4  27650  wlkiswwlks2lem5  27651  wwlksnfiOLD  27685  clwwlkvbij  27892  konigsbergumgr  28030  ex-pw  28208  ex-xp  28215  ex-rn  28219  nvvop  28386  nvm  28418  cnims  28470  ip0i  28602  ip1ilem  28603  ipdirilem  28606  ipasslem10  28616  h2hva  28751  h2hsm  28752  h2hvs  28754  axhfvadd-zf  28759  axhvcom-zf  28760  axhvass-zf  28761  axhv0cl-zf  28762  axhvaddid-zf  28763  axhfvmul-zf  28764  axhvmulid-zf  28765  axhvmulass-zf  28766  axhvdistr1-zf  28767  axhvdistr2-zf  28768  axhvmul0-zf  28769  axhfi-zf  28770  axhis1-zf  28771  axhis2-zf  28772  axhis3-zf  28773  axhis4-zf  28774  axhcompl-zf  28775  normlem0  28886  normlem1  28887  normlem2  28888  normlem4  28890  normlem9  28895  bcseqi  28897  dfhnorm2  28899  norm3difi  28924  normpari  28931  normpar2i  28933  polid2i  28934  polidi  28935  hhba  28944  hhims  28949  hhims2  28950  hhsssh  29046  hhssims  29051  hhssims2  29052  shsval3i  29165  dfch2  29184  cmcm2i  29370  fh2  29396  qlaxr3i  29413  spansnji  29423  pjcji  29461  ho0val  29527  df0op2  29529  hosd1i  29599  hosd2i  29600  eigorthi  29614  hhlnoi  29677  hhnmoi  29678  hhbloi  29679  bra0  29727  nmop0  29763  nmfn0  29764  lnopeq0lem1  29782  lnopunilem1  29787  lnophmlem2  29794  nmopcoadji  29878  pjhmopidm  29960  cvmdi  30101  cdj3lem3  30215  cdj3lem3b  30217  abrexdomjm  30267  uniin1  30303  uniin2  30304  iundifdifd  30313  iundifdif  30314  mpomptxf  30425  df1stres  30439  df2ndres  30440  fcobijfs  30459  resf1o  30466  fpwrelmapffslem  30468  dpval3  30570  dp3mul10  30574  dpadd2  30586  dpmul4  30590  xrslt  30663  xrsclat  30667  xrge0tsmsd  30692  gsumle  30725  cycpmco2lem7  30774  cycpmconjv  30784  cycpmrn  30785  xrge0slmod  30917  rgmoddim  31008  circtopn  31101  tpr2rico  31155  xrge0mulc1cn  31184  lmxrge0  31195  esumpfinvallem  31333  esumcocn  31339  hasheuni  31344  esumcvg  31345  rossros  31439  measinblem  31479  aean  31503  sxbrsigalem3  31530  dya2iocival  31531  dya2iocucvr  31542  sxbrsigalem1  31543  sxbrsigalem2  31544  sxbrsigalem5  31546  sxbrsiga  31548  fiunelcarsg  31574  eulerpartlem1  31625  eulerpartgbij  31630  fibp1  31659  coinfliplem  31736  coinflipprob  31737  ballotlemfval  31747  ballotth  31795  sgnneg  31798  plymulx  31818  circlemethhgt  31914  hgt750lem2  31923  bnj1400  32107  bnj66  32132  bnj882  32198  lfuhgr  32364  derang0  32416  subfacp1lem1  32426  subfacp1lem6  32432  kur14lem7  32459  cvmsss2  32521  cvmliftlem8  32539  cvmliftlem10  32541  satfv1lem  32609  msubfval  32771  quad3  32913  bcprod  32970  bccolsum  32971  faclim  32978  dftrpred2  33058  bdayfo  33182  pprodcnveq  33344  dfon4  33354  fobigcup  33361  dfiota3  33384  dfrecs2  33411  dfrdg4  33412  dfint3  33413  rankeq1o  33632  refssfne  33706  ssoninhaus  33796  onint1  33797  bj-rababw  34200  bj-inrab3  34250  dissneq  34625  dffinxpf  34669  finxpreclem4  34678  wl-dfrabsb  34876  rabiun  34880  ptrest  34906  poimirlem3  34910  poimirlem4  34911  poimirlem13  34920  poimirlem16  34923  poimirlem22  34929  poimirlem26  34933  poimirlem27  34934  poimirlem30  34937  cnambfre  34955  ftc1anclem8  34989  fnopabco  35013  abrexdom  35020  cncfres  35058  scottexf  35461  scott0f  35462  inres2  35521  dfres4  35565  xrnres  35665  xrnres2  35666  dfcoss2  35676  dfcoss4  35678  1cossres  35689  dmcoss2  35709  1cosscnvxrn  35730  dfeqvrels2  35838  dfcoeleqvrels  35871  redundss3  35878  dffunsALTV5  35935  cdleme3d  37382  cdleme7a  37394  cdleme31sdnN  37538  cdlemk45  38098  420gcd8e4  39127  lcmeprodgcdi  39128  60lcm7e420  39131  420lcm8e840  39132  imaopab  39168  dfqs2  39171  dfqs3  39172  decaddcom  39219  nn0expgcd  39233  sn-00idlem2  39278  mapfzcons  39362  eldioph4b  39457  diophren  39459  pwssplit4  39738  pwfi2f1o  39745  frlmpwfi  39747  mendplusgfval  39834  mendmulrfval  39836  mendvscafval  39839  idomodle  39845  cytpval  39858  arearect  39871  tr3dom  39943  alephiso2  39966  alephiso3  39967  relintab  39992  dfid7  40021  cnvrcl0  40034  dfrtrcl5  40038  dfrcl3  40069  dfrcl4  40070  comptiunov2i  40100  corcltrcl  40133  neicvgnvo  40514  inductionexd  40554  mnuprdlem2  40658  nznngen  40697  hashnzfz2  40702  lhe4.4ex1a  40710  dvradcnv2  40728  binomcxplemrat  40731  binomcxplemnotnn0  40737  refsum2cnlem1  41343  fiiuncl  41376  iccdifprioo  41841  lptre2pt  41970  limclner  41981  stoweidlem13  42347  stoweidlem32  42366  stoweidlem62  42396  wallispi2lem2  42406  stirlinglem14  42421  dirkertrigeqlem1  42432  dirkercncflem4  42440  fourierdlem42  42483  fourierdlem73  42513  fourierdlem81  42521  fourierdlem92  42532  fourierdlem103  42543  fourierdlem104  42544  fouriercnp  42560  fouriersw  42565  sge0tsms  42711  sge0iunmptlemfi  42744  ovolval5lem3  42985  cnfsmf  43066  rnfdmpr  43529  fvmptrabdm  43541  fundcmpsurinjlem1  43607  m11nprm  43815  opoeALTV  43897  nfermltl8rev  43956  sbgoldbo  44001  evengpop3  44012  cznabel  44274  cznrng  44275  mpomptx2  44432  2sphere  44785  itscnhlinecirc02plem3  44820  inlinecirc02p  44823  amgmlemALT  44953