Theorem eqtr4i 2757

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 2740	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2754	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 2121  ax-ext 2703

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

This theorem is referenced by:  3eqtr2i  2760  3eqtr2ri  2761  3eqtr4i  2764  3eqtr4ri  2765  rabab  3467  cbvralcsf  3887  cbvrabcsf  3890  dfin5  3905  dfdif2  3906  uneqin  4236  notabw  4260  unrab  4262  inrab  4263  inrab2  4264  difrab  4265  dfrab3ss  4270  rabun2  4271  dfnul2  4283  difid  4323  rabxm  4337  elnelun  4340  abf  4353  difdifdir  4439  dfif3  4487  dfif5  4489  rabsnif  4673  tpidm  4708  ssunpr  4783  sstp  4785  opidg  4841  dfint2  4897  iunrab  4999  uniiun  5005  intiin  5006  iunid  5007  0iin  5010  mptv  5195  dfepfr  5598  epfrc  5599  xpundi  5683  xpundir  5684  csbcnv  5822  resiun2  5948  resopab  5982  mptresid  5999  dffr3  6047  dfse2  6048  cnvun  6089  imaundir  6097  imainrect  6128  cnvcnv2  6140  cnvrescnv  6142  cnvcnvres  6152  dmtpop  6165  rnsnopg  6168  resdifdi  6183  rnco2  6201  dmco  6202  co01  6209  unidmrn  6226  dfdm2  6228  predidm  6273  dfmpt3  6615  mptun  6627  funcocnv2  6788  dffv2  6917  fnasrn  7078  fpr  7087  fmptap  7104  rnmptc  7141  riotav  7308  dmoprab  7449  rnoprab2  7452  mpov  7458  mpomptx  7459  abrexex2g  7896  1stval2  7938  2ndval2  7939  fo1st  7941  fo2nd  7942  xp2  7958  dfoprab4f  7988  offval22  8018  fmpoco  8025  fimaproj  8065  tposmpo  8193  tposconst  8194  recsfval  8300  rdgsucmpt2  8349  frsucmpt2  8359  df2o3  8393  o1p1e2  8455  o2p2e4  8456  oarec  8477  omopthlem2  8575  ecqs  8703  qliftf  8729  erovlem  8737  fset0  8778  mapsnf1o3  8819  ixp0x  8850  omf1o  8993  xpf1o  9052  mapunen  9059  enp1ilem  9162  marypha1lem  9317  marypha2lem4  9322  dfoi  9397  infeq5i  9526  oemapso  9572  cantnflem1  9579  rankelop  9767  leweon  9902  r0weon  9903  kmlem11  10052  dju1dif  10064  ackbij1lem16  10125  cf0  10142  cfsmolem  10161  alephsuc3  10471  fpwwe  10537  canthp1lem1  10543  wuncval2  10638  prlem936  10938  m1p1sr  10983  m1m1sr  10984  dfcnqs  11033  ssxr  11182  mul02lem2  11290  addrid  11293  2p2e4  12255  3p2e5  12271  3p3e6  12272  4p2e6  12273  4p3e7  12274  4p4e8  12275  5p2e7  12276  5p3e8  12277  5p4e9  12278  6p2e8  12279  6p3e9  12280  7p2e9  12281  nnzrab  12500  nn0zrab  12501  dec0u  12609  dec0h  12610  decsuc  12619  decsucc  12629  numma  12632  decma  12639  decmac  12640  decma2c  12641  decadd  12642  decaddc  12643  decmul1c  12653  decmul2c  12654  5p5e10  12659  6p4e10  12660  7p3e10  12663  8p2e10  12668  5t5e25  12691  6t6e36  12696  8t6e48  12707  nn0uz  12774  nnuz  12775  xaddcom  13139  x2times  13198  ioomax  13322  iccmax  13323  ioopos  13324  ioorp  13325  prunioo  13381  fseq1p1m1  13498  fzo13pr  13649  fzo0to2pr  13650  fzo0to3tp  13652  om2uzrdg  13863  fzennn  13875  irec  14108  sq10e99m1  14172  facnn  14182  fac0  14183  faclbnd2  14198  faclbnd4lem1  14200  hashfun  14344  hashbclem  14359  hashf1lem1  14362  hashf1lem2  14363  fz1isolem  14368  swrdccatin1  14632  swrdccat3blem  14646  s1co  14740  s2eq2s1eq  14843  s3eqs2s1eq  14845  ofs2  14878  dfid5  14934  dfid6  14935  fsumrev2  15689  fsumparts  15713  fsumiun  15728  isumnn0nn  15749  harmonic  15766  fprod2d  15888  bpoly2  15964  bpoly3  15965  bpoly4  15966  ege2le3  15997  cos1bnd  16096  efieq1re  16108  eirrlem  16113  qnnen  16122  cpnnen  16138  ruclem6  16144  3dvds  16242  pwp1fsum  16302  m1bits  16351  nn0expgcd  16475  algrp1  16485  phiprmpw  16687  prmreclem4  16831  4sqlem11  16867  4sqlem19  16875  dec5dvds  16976  decsplit1  16993  5prm  17020  7prm  17022  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  strle1  17069  grpbasex  17196  grpplusgx  17197  quslem  17447  xpsrnbas  17475  acsfn1  17567  acsfn2  17569  comfffval2  17607  dfinito2  17910  dftermo2  17911  xpchomfval  18085  xpccofval  18088  1stfval  18097  2ndfval  18100  oduleg  18196  chnub  18528  ismgmid  18573  efmndbas  18779  smndex2dnrinv  18823  grpinvfvi  18895  gaorb  19219  elcntr  19242  cntri  19244  cntrsubgnsg  19255  cntrnsg  19256  setsplusg  19262  oppgcntr  19277  gsumwrev  19278  symgressbas  19294  symgplusg  19295  symgvalstruct  19309  symgga  19319  cayleylem1  19324  psgnunilem2  19407  efgval2  19636  efgredlemc  19657  efgcpbllema  19666  frgpnabllem1  19785  gsumzaddlem  19833  gsumle  20057  opprlem  20260  oppr0  20267  opprneg  20269  rmodislmod  20863  rlmscaf  21141  xrsds  21346  gsumfsum  21371  zringunit  21403  pzriprng1  21435  cnmsgngrp  21516  psgnfix2  21536  relt  21552  ocv0  21614  thlle  21634  thlleval  21635  dsmmval2  21673  frlmip  21715  mplbas  21927  mplplusg  21944  mplmulr  21945  mplvsca2  21951  ressmplbas2  21962  ltbwe  21979  evlslem4  22011  psdmul  22081  psr1bas2  22102  ply1bas  22107  ply1basOLD  22108  ply1assa  22112  psr1plusg  22133  psr1vsca  22134  psr1mulr  22135  ply1plusg  22136  ply1vsca  22137  ply1mulr  22138  ply1mpl0  22169  ply1mpl1  22171  coe1mul  22184  matgsum  22352  smadiadetglem1  22586  indistpsx  22925  iuncld  22960  tgrest  23074  resstopn  23101  leordtval2  23127  xkouni  23514  ptclsg  23530  ptuncnv  23722  ptunhmeo  23723  alexsubALTlem4  23965  tsmsf1o  24060  ucnimalem  24194  ressxms  24440  uniretop  24677  cnfldtopn  24696  xrtgioo  24722  zcld  24729  icccmp  24741  xrge0gsumle  24749  xrge0tsms  24750  metnrmlem3  24777  fsum2cn  24789  cnmpopc  24849  oprpiece1res1  24876  oprpiece1res2  24877  evth  24885  evth2  24886  om1opn  24963  pi1xfrf  24980  pi1xfrcnv  24984  pi1cof  24986  clsocv  25177  cncmet  25249  cnflduss  25283  rrxprds  25316  ehlbase  25342  ismbl  25454  shftmbl  25466  ioorinv  25504  itg1addlem4  25627  itg2cnlem1  25689  itg0  25708  itgss3  25743  ditgneg  25785  limcdif  25804  limciun  25822  dvexp  25884  dvef  25911  dvcnvrelem2  25950  ftc1  25976  aannenlem2  26264  dvradcnv  26357  pserdvlem2  26365  reefgim  26387  cospi  26408  sincos6thpi  26452  tanregt0  26475  dflog2  26496  logfac  26537  dvlog  26587  cxpexp  26604  cxpmul2  26625  cxpsqrt  26639  dvsqrt  26678  dvcnsqrt  26680  cxpcn2  26683  isosctrlem2  26756  1cubrlem  26778  1cubr  26779  quart1lem  26792  atancj  26847  atanlogaddlem  26850  atansopn  26869  leibpilem2  26878  log2cnv  26881  log2ublem3  26885  birthdaylem1  26888  birthdaylem2  26889  birthday  26891  dfarea  26897  lgamgulmlem5  26970  lgambdd  26974  ftalem3  27012  basellem2  27019  ppiprm  27088  ppinprm  27089  chtprm  27090  chtnprm  27091  ppi2  27107  ppi3  27108  ppiub  27142  chtub  27150  bclbnd  27218  bposlem8  27229  lgsdilem  27262  lgsdir2lem2  27264  lgsquadlem2  27319  lgsquad2lem2  27323  2lgsoddprmlem3c  27350  rplogsum  27465  mulog2sumlem2  27473  pnt2  27551  bdayfo  27616  bday0s  27772  bday1s  27775  old1  27820  addsasslem2  27947  negsbdaylem  27998  muls01  28051  abssnid  28181  1p1e2s  28339  n0seo  28344  twocut  28346  halfcut  28378  pw2cutp1  28381  pw2cut2  28382  zs12bday  28394  istrkg2ld  28438  axsegconlem9  28903  ax5seglem7  28913  iedgedg  29028  uspgrf1oedg  29151  nbgrcl  29313  nbgrnvtx0  29317  rusgrprc  29569  pthsfval  29697  wlkiswwlks2lem4  29850  wlkiswwlks2lem5  29851  clwwlkvbij  30093  konigsbergumgr  30231  ex-pw  30409  ex-xp  30416  ex-rn  30420  nvvop  30589  nvm  30621  cnims  30673  ip0i  30805  ip1ilem  30806  ipdirilem  30809  ipasslem10  30819  h2hva  30954  h2hsm  30955  h2hvs  30957  axhfvadd-zf  30962  axhvcom-zf  30963  axhvass-zf  30964  axhv0cl-zf  30965  axhvaddid-zf  30966  axhfvmul-zf  30967  axhvmulid-zf  30968  axhvmulass-zf  30969  axhvdistr1-zf  30970  axhvdistr2-zf  30971  axhvmul0-zf  30972  axhfi-zf  30973  axhis1-zf  30974  axhis2-zf  30975  axhis3-zf  30976  axhis4-zf  30977  axhcompl-zf  30978  normlem0  31089  normlem1  31090  normlem2  31091  normlem4  31093  normlem9  31098  bcseqi  31100  dfhnorm2  31102  norm3difi  31127  normpari  31134  normpar2i  31136  polid2i  31137  polidi  31138  hhba  31147  hhims  31152  hhims2  31153  hhsssh  31249  hhssims  31254  hhssims2  31255  shsval3i  31368  dfch2  31387  cmcm2i  31573  fh2  31599  qlaxr3i  31616  spansnji  31626  pjcji  31664  ho0val  31730  df0op2  31732  hosd1i  31802  hosd2i  31803  eigorthi  31817  hhlnoi  31880  hhnmoi  31881  hhbloi  31882  bra0  31930  nmop0  31966  nmfn0  31967  lnopeq0lem1  31985  lnopunilem1  31990  lnophmlem2  31997  nmopcoadji  32081  pjhmopidm  32163  cvmdi  32304  cdj3lem3  32418  cdj3lem3b  32420  abrexdomjm  32487  uniin1  32531  uniin2  32532  iundifdifd  32541  iundifdif  32542  mpomptxf  32659  df1stres  32685  df2ndres  32686  intimafv  32692  fcobijfs  32704  fcobijfs2  32705  resf1o  32713  fpwrelmapffslem  32715  sgnneg  32816  dpval3  32874  dp3mul10  32878  dpadd2  32890  dpmul4  32894  ccatws1f1o  32932  xrslt  32988  xrsclat  32992  xrge0tsmsd  33042  cycpmco2lem7  33101  cycpmconjv  33111  cycpmrn  33112  conjga  33139  elrgspnsubrunlem2  33215  rndrhmcl  33262  fracf1  33273  xrge0slmod  33313  lsmsnorb2  33357  qusbas2  33371  1arithidomlem2  33501  zringfrac  33519  mplvrpmga  33575  mplvrpmmhm  33576  mplvrpmrhm  33577  rlmdim  33622  rgmoddimOLD  33623  isconstr  33749  iconstr  33779  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  circtopn  33850  tpr2rico  33925  xrge0mulc1cn  33954  lmxrge0  33965  esumpfinvallem  34087  esumcocn  34093  hasheuni  34098  esumcvg  34099  rossros  34193  measinblem  34233  aean  34257  sxbrsigalem3  34285  dya2iocival  34286  dya2iocucvr  34297  sxbrsigalem1  34298  sxbrsigalem2  34299  sxbrsigalem5  34301  sxbrsiga  34303  fiunelcarsg  34329  eulerpartlem1  34380  eulerpartgbij  34385  fibp1  34414  coinfliplem  34492  coinflipprob  34493  ballotlemfval  34503  ballotth  34551  plymulx  34561  circlemethhgt  34656  hgt750lem2  34665  bnj1400  34847  bnj66  34872  bnj882  34938  lfuhgr  35162  derang0  35213  subfacp1lem1  35223  subfacp1lem6  35229  kur14lem7  35256  cvmsss2  35318  cvmliftlem8  35336  cvmliftlem10  35338  satfv1lem  35406  msubfval  35568  quad3  35714  bcprod  35782  bccolsum  35783  faclim  35790  pprodcnveq  35925  dfon4  35935  fobigcup  35942  dfiota3  35965  dfrecs2  35994  dfrdg4  35995  dfint3  35996  rankeq1o  36215  refssfne  36402  ssoninhaus  36492  onint1  36493  bj-rababw  36925  bj-inrab3  36973  bj-imdiridlem  37229  dissneq  37385  dffinxpf  37429  finxpreclem4  37438  rabiun  37643  ptrest  37669  poimirlem3  37673  poimirlem4  37674  poimirlem13  37683  poimirlem16  37686  poimirlem22  37692  poimirlem26  37696  poimirlem27  37697  poimirlem30  37700  cnambfre  37718  ftc1anclem8  37750  fnopabco  37773  abrexdom  37780  cncfres  37815  scottexf  38218  scott0f  38219  inres2  38292  dfres4  38341  dmxrn  38421  xrnres  38459  xrnres2  38460  dfsucmap2  38487  dfcoss2  38525  dfcoss4  38527  1cossres  38541  dmcoss2  38566  1cosscnvxrn  38587  dfeqvrels2  38694  dfcoeleqvrels  38727  redundss3  38734  dffunsALTV5  38795  cdleme3d  40340  cdleme7a  40352  cdleme31sdnN  40496  cdlemk45  41056  420gcd8e4  42109  lcmeprodgcdi  42110  60lcm7e420  42113  420lcm8e840  42114  3lexlogpow5ineq1  42157  3lexlogpow2ineq1  42161  3lexlogpow2ineq2  42162  3lexlogpow5ineq5  42163  aks4d1p1  42179  posbezout  42203  aks6d1c1p4  42214  aks6d1c3  42226  2ap1caineq  42248  sticksstones7  42255  sticksstones12a  42260  sticksstones12  42261  aks6d1c6lem4  42276  imaopab  42334  fmpocos  42337  dfqs2  42340  dfqs3  42341  decaddcom  42387  sumcubes  42416  redvmptabs  42463  readvrec  42465  readvcot  42467  sn-00idlem2  42502  reixi  42526  sum9cubes  42775  mapfzcons  42819  eldioph4b  42914  diophren  42916  pwssplit4  43192  pwfi2f1o  43199  frlmpwfi  43201  mendplusgfval  43284  mendmulrfval  43286  mendvscafval  43289  idomodle  43294  cytpval  43305  arearect  43318  onov0suclim  43377  omabs2  43435  tr3dom  43631  har2o  43649  alephiso2  43661  alephiso3  43662  relintab  43686  dfid7  43715  cnvrcl0  43728  dfrtrcl5  43732  dfrcl3  43778  dfrcl4  43779  comptiunov2i  43809  corcltrcl  43842  neicvgnvo  44218  inductionexd  44258  mnuprdlem2  44376  nznngen  44419  hashnzfz2  44424  lhe4.4ex1a  44432  dvradcnv2  44450  binomcxplemrat  44453  binomcxplemnotnn0  44459  nregmodelf1o  45118  refsum2cnlem1  45144  fiiuncl  45172  iccdifprioo  45626  lptre2pt  45748  limclner  45759  stoweidlem13  46121  stoweidlem32  46140  stoweidlem62  46170  wallispi2lem2  46180  stirlinglem14  46195  dirkertrigeqlem1  46206  dirkercncflem4  46214  fourierdlem42  46257  fourierdlem73  46287  fourierdlem81  46295  fourierdlem92  46306  fourierdlem103  46317  fourierdlem104  46318  fouriercnp  46334  fouriersw  46339  sge0tsms  46488  sge0iunmptlemfi  46521  ovolval5lem3  46762  cnfsmf  46848  nthrucw  46994  lamberte  46998  rnfdmpr  47391  fvmptrabdm  47403  fundcmpsurinjlem1  47508  m11nprm  47711  opoeALTV  47793  nfermltl8rev  47852  sbgoldbo  47897  evengpop3  47908  clnbgrcl  47931  clnbgrnvtx0  47937  usgrexmpl2edg  48139  usgrexmpl2nb0  48141  usgrexmpl2nb3  48144  gpg5order  48170  gpgprismgr4cycllem6  48210  cznabel  48370  cznrng  48371  mpomptx2  48445  2sphere  48860  itscnhlinecirc02plem3  48895  inlinecirc02p  48898  dftpos5  48984  tposresg  48988  icccldii  49029  dfnrm2  49042  dfnrm3  49043  elxpcbasex1ALT  49360  elxpcbasex2ALT  49362  dfswapf2  49372  swapf1a  49380  swapf1f1o  49386  swapf2f1oa  49388  swapfida  49391  setc1oterm  49602  setc1ohomfval  49604  setc1ocofval  49605  funcsetc1o  49608  dfinito4  49612  setc1onsubc  49713  islmd  49776  iscmd  49777  initocmd  49780  termolmd  49781  amgmlemALT  49914