Theorem eqtr4i 2786

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 2769	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2783	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 2155  ax-ext 2732

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

This theorem is used by:  3eqtr2i  2789  3eqtr2ri  2790  3eqtr4i  2793  3eqtr4ri  2794  rabab  3480  cbvralcsf  3889  cbvrabcsf  3892  dfin5  3907  dfdif2  3908  uneqin  4235  notabw  4259  unrab  4261  inrab  4262  inrab2  4263  difrab  4264  dfrab3ss  4269  rabun2  4270  dfnul2  4282  difid  4325  rabxm  4340  elnelun  4343  abf  4364  difdifdir  4447  dfif3  4497  dfif5  4499  rabsnif  4684  tpidm  4719  ssunpr  4794  sstp  4796  opidg  4852  dfint2  4909  iunrab  5011  uniiun  5017  intiin  5018  iunid  5019  0iin  5022  uniin1  5033  uniin2  5034  mptv  5211  dfepfr  5639  epfrc  5640  xpundi  5724  xpundir  5725  csbcnv  5866  csbcnvOLD  5867  resiun2  5993  resopab  6030  mptresid  6047  dffr3  6095  dfse2  6096  cnvun  6133  imaundir  6142  imainrect  6174  cnvcnv2  6186  cnvrescnv  6189  cnvcnvres  6201  dmtpop  6214  rnsnopg  6217  resdifdi  6232  rnco2  6250  dmco  6251  co01  6258  unidmrn  6277  dfdm2  6279  predidm  6324  dfmpt3  6667  mptun  6679  funcocnv2  6844  dffv2  6974  fnasrn  7142  fpr  7152  fmptap  7169  rnmptc  7207  riotav  7376  dmoprab  7517  rnoprab2  7520  mpov  7526  mpomptx  7527  abrexex2g  7962  1stval2  8004  2ndval2  8005  fo1st  8007  fo2nd  8008  xp2  8024  dfoprab4f  8054  offval22  8086  fmpoco  8093  fimaproj  8134  tposmpo  8262  tposconst  8263  recsfval  8370  rdgsucmpt2  8420  frsucmpt2  8430  df2o3  8464  o1p1e2  8528  o2p2e4  8529  oarec  8550  omopthlem2  8649  dfqs2  8704  ecqs  8780  qliftf  8806  erovlem  8814  fset0  8856  mapsnf1o3  8903  ixp0x  8934  omf1o  9079  xpf1o  9138  mapunen  9145  enp1ilem  9249  marypha1lem  9404  marypha2lem4  9409  dfoi  9484  infeq5i  9616  oemapso  9662  cantnflem1  9669  rankelop  9857  leweon  10015  r0weon  10016  kmlem11  10164  dju1dif  10176  ackbij1lem16  10237  cf0  10253  cfsmolem  10273  alephsuc3  10590  fpwwe  10656  canthp1lem1  10662  wuncval2  10757  prlem936  11057  m1p1sr  11102  m1m1sr  11103  dfcnqs  11152  ssxr  11304  mul02lem2  11412  addrid  11415  2p2e4  12400  3p2e5  12416  3p3e6  12417  4p2e6  12418  4p3e7  12419  4p4e8  12420  5p2e7  12421  5p3e8  12422  5p4e9  12423  6p2e8  12424  6p3e9  12425  7p2e9  12426  nnzrab  12647  nn0zrab  12648  dec0u  12763  dec0h  12764  decsuc  12773  decsucc  12783  numma  12786  decma  12793  decmac  12794  decma2c  12795  decadd  12796  decaddc  12797  decmul1c  12807  decmul2c  12808  5p5e10  12813  6p4e10  12814  7p3e10  12817  8p2e10  12822  5t5e25  12845  6t6e36  12850  8t6e48  12861  nn0uz  12926  nnuz  12927  xaddcom  13293  x2times  13352  ioomax  13476  iccmax  13477  ioopos  13478  ioorp  13479  prunioo  13535  fseq1p1m1  13654  fzo13pr  13806  fzo0to2pr  13807  fzo0to3tp  13809  om2uzrdg  14021  fzennn  14033  irec  14266  sq10e99m1  14330  facnn  14340  fac0  14341  faclbnd2  14356  faclbnd4lem1  14358  hashfun  14503  hashbclem  14518  hashf1lem1  14521  hashf1lem2  14522  fz1isolem  14527  swrdccatin1  14795  swrdccat3blem  14809  s1co  14905  s2eq2s1eq  15008  s3eqs2s1eq  15010  ofs2  15045  dfid5  15101  dfid6  15102  sgnneg  15174  fsumrev2  15869  fsumparts  15894  fsumiun  15909  isumnn0nn  15932  harmonic  15949  fprod2d  16069  bpoly2  16144  bpoly3  16145  bpoly4  16146  ege2le3  16177  cos1bnd  16276  efieq1re  16288  eirrlem  16293  qnnen  16302  cpnnen  16318  ruclem6  16324  3dvds  16422  pwp1fsum  16482  m1bits  16531  nn0expgcd  16655  algrp1  16665  phiprmpw  16868  prmreclem4  17012  4sqlem11  17048  4sqlem19  17056  dec5dvds  17157  decsplit1  17174  5prm  17201  7prm  17203  1259lem2  17225  1259lem3  17226  1259lem4  17227  1259lem5  17228  1259prm  17229  2503lem1  17230  2503lem2  17231  2503lem3  17232  2503prm  17233  4001lem1  17234  4001lem2  17235  4001lem3  17236  4001lem4  17237  4001prm  17238  strle1  17251  grpbasex  17378  grpplusgx  17379  quslem  17630  xpsrnbas  17658  acsfn1  17750  acsfn2  17752  comfffval2  17790  dfinito2  18093  dftermo2  18094  xpchomfval  18268  xpccofval  18271  1stfval  18280  2ndfval  18283  oduleg  18379  chnub  18711  ismgmid  18759  efmndbas  18981  smndex2dnrinv  19028  degenmgmbas  19049  degenmgm2opdm  19052  grpinvfvi  19107  gaorb  19435  elcntr  19458  cntri  19460  cntrsubgnsg  19471  cntrnsg  19472  setsplusg  19478  oppgcntr  19493  gsumwrev  19494  symgressbas  19510  symgplusg  19511  symgvalstruct  19525  symgga  19535  cayleylem1  19540  psgnunilem2  19623  efgval2  19852  efgredlemc  19873  efgcpbllema  19882  frgpnabllem1  20001  gsumzaddlem  20049  gsumle  20273  opprlem  20484  oppr0  20491  opprneg  20493  rmodislmod  21115  rlmscaf  21392  xrsds  21624  gsumfsum  21648  zringunit  21680  pzriprng1  21712  cnmsgngrp  21793  psgnfix2  21813  relt  21829  ocv0  21891  thlle  21911  thlleval  21912  dsmmval2  21950  frlmip  21992  mplbas  22205  mplplusg  22222  mplmulr  22223  mplvsca2  22229  ressmplbas2  22243  ltbwe  22261  evlslem4  22293  psdmul  22395  psr1bas2  22416  ply1bas  22421  ply1assa  22425  psr1plusg  22446  psr1vsca  22447  psr1mulr  22448  ply1plusg  22449  ply1vsca  22450  ply1mulr  22451  ply1mpl0  22482  ply1mpl1  22484  coe1mul  22497  matgsum  22660  smadiadetglem1  22894  indistpsx  23236  iuncld  23271  tgrest  23385  resstopn  23412  leordtval2  23438  xkouni  23826  ptclsg  23842  ptuncnv  24034  ptunhmeo  24035  alexsubALTlem4  24277  tsmsf1o  24372  ucnimalem  24506  ressxms  24752  uniretop  24989  cnfldtopn  25008  xrtgioo  25034  zcld  25041  icccmp  25053  xrge0gsumle  25061  xrge0tsms  25062  metnrmlem3  25089  fsum2cn  25100  cnmpopc  25157  oprpiece1res1  25180  oprpiece1res2  25181  evth  25188  evth2  25189  om1opn  25265  pi1xfrf  25282  pi1xfrcnv  25286  pi1cof  25288  clsocv  25479  cncmet  25551  cnflduss  25585  rrxprds  25618  ehlbase  25644  ismbl  25755  shftmbl  25767  ioorinv  25805  itg1addlem4  25928  itg2cnlem1  25990  itg0  26008  itgss3  26043  ditgneg  26085  limcdif  26104  limciun  26122  dvexp  26181  dvef  26208  dvcnvrelem2  26246  ftc1  26270  plymulidp  26513  aannenlem2  26566  dvradcnv  26658  pserdvlem2  26665  reefgim  26687  cospi  26711  sincos6thpi  26754  tanregt0  26777  dflog2  26798  logfac  26839  dvlog  26889  cxpexp  26906  cxpmul2  26927  cxpsqrt  26941  dvsqrt  26980  dvcnsqrt  26982  cxpcn2  26984  isosctrlem2  27057  1cubrlem  27079  1cubr  27080  quart1lem  27093  atancj  27148  atanlogaddlem  27151  atansopn  27170  leibpilem2  27179  log2cnv  27182  log2ublem3  27186  birthdaylem1  27189  birthdaylem2  27190  birthday  27192  dfarea  27198  lgamgulmlem5  27270  lgambdd  27274  ftalem3  27312  basellem2  27319  ppiprm  27388  ppinprm  27389  chtprm  27390  chtnprm  27391  ppi2  27407  ppi3  27408  ppiub  27441  chtub  27449  bclbnd  27517  bposlem8  27528  lgsdilem  27561  lgsdir2lem2  27563  lgsquadlem2  27618  lgsquad2lem2  27622  2lgsoddprmlem3c  27649  rplogsum  27764  mulog2sumlem2  27772  pnt2  27850  bdayfo  27914  bday0  28077  bday1  28080  old1  28131  addsasslem2  28270  negbdaylem  28322  muls01  28378  abssnid  28509  1p1e2s  28682  n0seo  28687  twocut  28689  halfcut  28724  pw2cutp1  28727  pw2cut2  28728  istrkg2ld  28802  axsegconlem9  29383  ax5seglem7  29393  iedgedg  29508  lfuhgr  29606  uspgrf1oedg  29634  nbgrcl  29796  nbgrnvtx0  29800  rusgrprc  30051  pthsfval  30184  wlkiswwlks2lem4  30341  wlkiswwlks2lem5  30342  clwwlkvbij  30584  konigsbergumgr  30732  ex-pw  30910  ex-xp  30917  ex-rn  30921  nvvop  31091  nvm  31123  cnims  31175  ip0i  31307  ip1ilem  31308  ipdirilem  31311  ipasslem10  31321  h2hva  31456  h2hsm  31457  h2hvs  31459  axhfvadd-zf  31464  axhvcom-zf  31465  axhvass-zf  31466  axhv0cl-zf  31467  axhvaddid-zf  31468  axhfvmul-zf  31469  axhvmulid-zf  31470  axhvmulass-zf  31471  axhvdistr1-zf  31472  axhvdistr2-zf  31473  axhvmul0-zf  31474  axhfi-zf  31475  axhis1-zf  31476  axhis2-zf  31477  axhis3-zf  31478  axhis4-zf  31479  axhcompl-zf  31480  normlem0  31591  normlem1  31592  normlem2  31593  normlem4  31595  normlem9  31600  bcseqi  31602  dfhnorm2  31604  norm3difi  31629  normpari  31636  normpar2i  31638  polid2i  31639  polidi  31640  hhba  31649  hhims  31654  hhims2  31655  hhsssh  31751  hhssims  31756  hhssims2  31757  shsval3i  31870  dfch2  31889  cmcm2i  32075  fh2  32101  qlaxr3i  32118  spansnji  32128  pjcji  32166  ho0val  32232  df0op2  32234  hosd1i  32304  hosd2i  32305  eigorthi  32319  hhlnoi  32382  hhnmoi  32383  hhbloi  32384  bra0  32432  nmop0  32468  nmfn0  32469  lnopeq0lem1  32487  lnopunilem1  32492  lnophmlem2  32499  nmopcoadji  32583  pjhmopidm  32665  cvmdi  32806  cdj3lem3  32920  cdj3lem3b  32922  abrexdomjm  32983  iundifdifd  33036  iundifdif  33037  mpomptxf  33152  df1stres  33177  df2ndres  33178  intimafv  33184  fcobijfs  33193  fcobijfs2  33194  resf1o  33202  fpwrelmapffslem  33204  dpval3  33340  dp3mul10  33344  dpadd2  33356  dpmul4  33360  ccatws1f1o  33394  xrslt  33448  xrsclat  33452  xrge0tsmsd  33514  cycpmco2lem7  33573  cycpmconjv  33583  cycpmrn  33584  conjga  33611  elrgspnsubrunlem2  33689  rndrhmcl  33738  fracf1  33749  xrge0slmod  33789  lsmsnorb2  33826  qusbas2  33836  1arithidomlem2  33947  zringfrac  33965  selvply1rhm0  34037  mplvrpmga  34056  mplvrpmmhm  34057  mplvrpmrhm  34058  psrmonprod  34063  mplmonprod  34065  vieta  34091  rlmdim  34121  isconstr  34247  iconstr  34277  cos9thpiminplylem4  34296  cos9thpiminplylem5  34297  circtopn  34348  tpr2rico  34423  xrge0mulc1cn  34452  lmxrge0  34463  esumpfinvallem  34585  esumcocn  34591  hasheuni  34596  esumcvg  34597  rossros  34692  measinblem  34732  aean  34756  sxbrsigalem3  34784  dya2iocival  34785  dya2iocucvr  34796  sxbrsigalem1  34797  sxbrsigalem2  34798  sxbrsigalem5  34800  sxbrsiga  34802  fiunelcarsg  34828  eulerpartlem1  34879  eulerpartgbij  34884  fibp1  34913  coinfliplem  34991  coinflipprob  34992  ballotlemfval  35002  ballotth  35050  circlemethhgt  35152  hgt750lem2  35161  bnj1400  35345  bnj66  35370  bnj882  35436  dfscott2  35626  dfscott3  35627  derang0  35749  subfacp1lem1  35759  subfacp1lem6  35765  kur14lem7  35792  cvmsss2  35854  cvmliftlem8  35872  cvmliftlem10  35874  satfv1lem  35942  msubfval  36104  quad3  36250  bcprod  36318  bccolsum  36319  faclim  36326  pprodcnveq  36461  dfon4  36471  fobigcup  36478  dfiota3  36501  dfrecs2  36530  dfrdg4  36531  dfint3  36532  rankeq1o  36752  refssfne  36978  ssoninhaus  37068  onint1  37069  ttciun  37134  bj-dfnul2  37272  bj-rababw  37625  bj-inrab3  37674  bj-imdiridlem  37938  dissneq  38096  dffinxpf  38140  finxpreclem4  38149  rabiun  38353  ptrest  38369  poimirlem3  38373  poimirlem4  38374  poimirlem13  38383  poimirlem16  38386  poimirlem22  38392  poimirlem26  38396  poimirlem27  38397  poimirlem30  38400  cnambfre  38418  ftc1anclem8  38450  fnopabco  38474  abrexdom  38481  cncfres  38516  scottexf  38917  scott0f  38918  inres2  38996  eqrabi  39005  xpv  39011  dfres4  39048  dmxrn  39136  xrnres  39174  xrnres2  39175  rnqmap  39203  dfsucmap2  39213  dfcoss2  39252  dfcoss4  39254  1cossres  39268  dmcoss2  39293  1cosscnvxrn  39314  dfeqvrels2  39421  dfcoeleqvrels  39454  redundss3  39461  dffunsALTV5  39521  dfpeters2  39723  cdleme3d  41105  cdleme7a  41117  cdleme31sdnN  41261  cdlemk45  41821  420gcd8e4  42873  lcmeprodgcdi  42874  60lcm7e420  42877  420lcm8e840  42878  3lexlogpow5ineq1  42921  3lexlogpow2ineq1  42925  3lexlogpow2ineq2  42926  3lexlogpow5ineq5  42927  aks4d1p1  42943  posbezout  42967  aks6d1c1p4  42978  aks6d1c3  42990  2ap1caineq  43012  sticksstones7  43019  sticksstones12a  43024  sticksstones12  43025  aks6d1c6lem4  43040  25or6to4  43073  imaopab  43102  fmpocos  43104  dfqs3  43107  decaddcom  43160  sumcubes  43189  redvmptabs  43236  readvrec  43238  readvcot  43240  sn-00idlem2  43275  reixi  43299  sum9cubes  43519  mapfzcons  43562  eldioph4b  43653  diophren  43655  pwssplit4  43931  pwfi2f1o  43938  frlmpwfi  43940  mendplusgfval  44023  mendmulrfval  44025  mendvscafval  44028  idomodle  44033  cytpval  44044  arearect  44057  onov0suclim  44116  omabs2  44174  tr3dom  44369  har2o  44387  alephiso2  44399  alephiso3  44400  relintab  44424  dfid7  44453  cnvrcl0  44466  dfrtrcl5  44470  dfrcl3  44516  dfrcl4  44517  comptiunov2i  44547  corcltrcl  44580  neicvgnvo  44956  inductionexd  44996  mnuprdlem2  45098  nznngen  45141  hashnzfz2  45146  lhe4.4ex1a  45154  dvradcnv2  45172  binomcxplemrat  45175  binomcxplemnotnn0  45181  nregmodelf1o  45839  refsum2cnlem1  45872  fiiuncl  45900  iccdifprioo  46347  lptre2pt  46469  limclner  46480  stoweidlem13  46842  stoweidlem32  46861  stoweidlem62  46891  wallispi2lem2  46901  stirlinglem14  46916  dirkertrigeqlem1  46927  dirkercncflem4  46935  fourierdlem42  46978  fourierdlem73  47008  fourierdlem81  47016  fourierdlem92  47027  fourierdlem103  47038  fourierdlem104  47039  fouriercnp  47055  fouriersw  47060  sge0tsms  47209  sge0iunmptlemfi  47242  ovolval5lem3  47483  cnfsmf  47569  goldpolyfactor  47746  goldratval  47755  lamberte  47757  rnfdmpr  48170  fvmptrabdm  48182  fundcmpsurinjlem1  48299  m11nprm  48505  ppi1sum  48535  opoeALTV  48600  nfermltl8rev  48659  sbgoldbo  48704  evengpop3  48715  clnbgrcl  48738  clnbgrnvtx0  48744  usgrexmpl2edg  48946  usgrexmpl2nb0  48948  usgrexmpl2nb3  48951  gpg5order  48977  gpgprismgr4cycllem6  49017  cznabel  49176  cznrng  49177  mpomptx2  49266  2sphere  49680  itscnhlinecirc02plem3  49715  inlinecirc02p  49718  dftpos5  49801  tposresg  49805  icccldii  49846  dfnrm2  49859  dfnrm3  49860  elxpcbasex1ALT  50176  elxpcbasex2ALT  50178  dfswapf2  50188  swapf1a  50196  swapf1f1o  50202  swapf2f1oa  50204  swapfida  50207  setc1oterm  50418  setc1ohomfval  50420  setc1ocofval  50421  funcsetc1o  50424  dfinito4  50428  setc1onsubc  50529  islmd  50592  iscmd  50593  initocmd  50596  termolmd  50597  dvsec  50690  dvcsc  50691  dvcot  50692  amgmlemALT  50822