Theorem eqtr4i 2787

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 2770	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2784	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 2733

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

This theorem is used by:  3eqtr2i  2790  3eqtr2ri  2791  3eqtr4i  2794  3eqtr4ri  2795  rabab  3481  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  5635  epfrc  5636  xpundi  5720  xpundir  5721  csbcnv  5864  csbcnvOLD  5865  resiun2  5991  resopab  6026  mptresid  6043  dffr3  6097  dfse2  6098  cnvun  6133  imaundir  6142  imainrect  6173  cnvcnv2  6185  cnvrescnv  6188  cnvcnvres  6206  dmtpop  6219  rnsnopg  6222  resdifdi  6237  rnco2  6255  dmco  6256  co01  6263  unidmrn  6282  dfdm2  6284  predidm  6329  dfmpt3  6673  mptun  6685  funcocnv2  6850  dffv2  6980  fnasrn  7148  fpr  7158  fmptap  7175  rnmptc  7213  riotav  7382  dmoprab  7523  rnoprab2  7526  mpov  7532  mpomptx  7533  abrexex2g  7976  1stval2  8018  2ndval2  8019  fo1st  8021  fo2nd  8022  xp2  8038  dfoprab4f  8067  offval22  8099  fmpoco  8106  fimaproj  8152  tposmpo  8280  tposconst  8281  recsfval  8388  rdgsucmpt2  8438  frsucmpt2  8448  df2o3  8484  o1p1e2  8548  o2p2e4  8549  oarec  8570  omopthlem2  8669  dfqs2  8724  ecqs  8800  qliftf  8826  erovlem  8834  fset0  8876  mapsnf1o3  8923  ixp0x  8954  omf1o  9099  xpf1o  9158  mapunen  9165  enp1ilem  9269  marypha1lem  9425  marypha2lem4  9430  dfoi  9505  infeq5i  9637  oemapso  9683  cantnflem1  9690  rankelop  9891  leweon  10090  r0weon  10091  kmlem11  10239  dju1dif  10251  ackbij1lem16  10312  cf0  10328  cfsmolem  10348  alephsuc3  10665  fpwwe  10731  canthp1lem1  10737  wuncval2  10832  prlem936  11132  m1p1sr  11177  m1m1sr  11178  dfcnqs  11227  ssxr  11379  mul02lem2  11487  addrid  11490  2p2e4  12477  3p2e5  12493  3p3e6  12494  4p2e6  12495  4p3e7  12496  4p4e8  12497  5p2e7  12498  5p3e8  12499  5p4e9  12500  6p2e8  12501  6p3e9  12502  7p2e9  12503  nnzrab  12724  nn0zrab  12725  dec0u  12840  dec0h  12841  decsuc  12850  decsucc  12860  numma  12863  decma  12870  decmac  12871  decma2c  12872  decadd  12873  decaddc  12874  decmul1c  12884  decmul2c  12885  5p5e10  12890  6p4e10  12891  7p3e10  12894  8p2e10  12899  5t5e25  12922  6t6e36  12927  8t6e48  12938  nn0uz  13003  nnuz  13004  xaddcom  13370  x2times  13429  ioomax  13553  iccmax  13554  ioopos  13555  ioorp  13556  prunioo  13612  fseq1p1m1  13732  fzo13pr  13884  fzo0to2pr  13885  fzo0to3tp  13887  om2uzrdg  14099  fzennn  14111  irec  14345  sq10e99m1  14409  facnn  14419  fac0  14420  faclbnd2  14435  faclbnd4lem1  14437  hashfun  14582  hashbclem  14597  hashf1lem1  14600  hashf1lem2  14601  fz1isolem  14606  swrdccatin1  14874  swrdccat3blem  14888  s1co  14984  s2eq2s1eq  15087  s3eqs2s1eq  15089  ofs2  15124  dfid5  15180  dfid6  15181  sgnneg  15253  fsumrev2  15948  fsumparts  15973  fsumiun  15988  isumnn0nn  16011  harmonic  16028  fprod2d  16148  bpoly2  16223  bpoly3  16224  bpoly4  16225  ege2le3  16256  cos1bnd  16355  efieq1re  16367  eirrlem  16372  qnnen  16381  cpnnen  16397  ruclem6  16403  3dvds  16501  pwp1fsum  16561  m1bits  16610  nn0expgcd  16738  algrp1  16749  phiprmpw  16953  prmreclem4  17097  4sqlem11  17133  4sqlem19  17141  dec5dvds  17242  decsplit1  17259  5prm  17286  7prm  17288  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  1259prm  17314  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001lem4  17322  4001prm  17323  strle1  17336  grpbasex  17463  grpplusgx  17464  quslem  17715  xpsrnbas  17743  acsfn1  17835  acsfn2  17837  comfffval2  17875  dfinito2  18178  dftermo2  18179  xpchomfval  18353  xpccofval  18356  1stfval  18365  2ndfval  18368  oduleg  18464  chnub  18796  idvalriota  18841  ismgmid  18845  efmndbas  19067  smndex2dnrinv  19114  degenmgmbas  19135  degenmgm2opdm  19138  grpinvfvi  19193  gaorb  19521  elcntr  19544  cntri  19546  cntrsubgnsg  19557  cntrnsg  19558  setsplusg  19564  oppgcntr  19579  gsumwrev  19580  symgressbas  19596  symgplusg  19597  symgvalstruct  19611  symgga  19621  cayleylem1  19626  psgnunilem2  19709  efgval2  19938  efgredlemc  19959  efgcpbllema  19968  frgpnabllem1  20087  gsumzaddlem  20135  gsumle  20359  opprlem  20572  oppr0  20579  opprneg  20581  rmodislmod  21205  rlmscaf  21482  xrsds  21716  gsumfsum  21740  zringunit  21772  pzriprng1  21804  cnmsgngrp  21885  psgnfix2  21905  relt  21921  ocv0  21983  thlle  22003  thlleval  22004  dsmmval2  22042  frlmip  22084  mplbas  22297  mplplusg  22314  mplmulr  22315  mplvsca2  22321  ressmplbas2  22335  ltbwe  22353  evlslem4  22385  psdmul  22487  psr1bas2  22508  ply1bas  22513  ply1assa  22517  psr1plusg  22538  psr1vsca  22539  psr1mulr  22540  ply1plusg  22541  ply1vsca  22542  ply1mulr  22543  ply1mpl0  22574  ply1mpl1  22576  coe1mul  22589  matgsum  22752  smadiadetglem1  22986  indistpsx  23328  iuncld  23363  tgrest  23477  resstopn  23504  leordtval2  23530  xkouni  23918  ptclsg  23934  ptuncnv  24126  ptunhmeo  24127  alexsubALTlem4  24369  tsmsf1o  24464  ucnimalem  24598  ressxms  24844  uniretop  25081  cnfldtopn  25100  xrtgioo  25126  zcld  25133  icccmp  25145  xrge0gsumle  25153  xrge0tsms  25154  metnrmlem3  25181  fsum2cn  25192  cnmpopc  25249  oprpiece1res1  25272  oprpiece1res2  25273  evth  25280  evth2  25281  om1opn  25357  pi1xfrf  25374  pi1xfrcnv  25378  pi1cof  25380  clsocv  25571  cncmet  25643  cnflduss  25677  rrxprds  25710  ehlbase  25736  ismbl  25847  shftmbl  25859  ioorinv  25897  itg1addlem4  26020  itg2cnlem1  26082  itg0  26100  itgss3  26135  ditgneg  26177  limcdif  26196  limciun  26214  dvexp  26273  dvef  26300  dvcnvrelem2  26338  ftc1  26362  plymulidp  26603  aannenlem2  26656  dvradcnv  26748  pserdvlem2  26755  reefgim  26777  cospi  26801  sincos6thpi  26844  tanregt0  26867  dflog2  26888  logfac  26929  dvlog  26979  cxpexp  26996  cxpmul2  27017  cxpsqrt  27031  dvsqrt  27070  dvcnsqrt  27072  cxpcn2  27074  isosctrlem2  27147  1cubrlem  27169  1cubr  27170  quart1lem  27183  atancj  27238  atanlogaddlem  27241  atansopn  27260  leibpilem2  27269  log2cnv  27272  log2ublem3  27276  birthdaylem1  27279  birthdaylem2  27280  birthday  27282  dfarea  27288  lgamgulmlem5  27360  lgambdd  27364  ftalem3  27402  basellem2  27409  ppiprm  27478  ppinprm  27479  chtprm  27480  chtnprm  27481  ppi2  27497  ppi3  27498  ppiub  27531  chtub  27539  bclbnd  27607  bposlem8  27618  lgsdilem  27651  lgsdir2lem2  27653  lgsquadlem2  27708  lgsquad2lem2  27712  2lgsoddprmlem3c  27739  rplogsum  27854  mulog2sumlem2  27862  pnt2  27940  fltoprmlem2  27994  bdayfo  28034  bday0  28197  bday1  28200  old1  28251  addsasslem2  28390  negbdaylem  28442  muls01  28498  abssnid  28629  1p1e2s  28802  n0seo  28807  twocut  28809  halfcut  28844  pw2cutp1  28847  pw2cut2  28848  istrkg2ld  28922  axsegconlem9  29503  ax5seglem7  29513  iedgedg  29628  lfuhgr  29726  uspgrf1oedg  29754  nbgrcl  29916  nbgrnvtx0  29920  rusgrprc  30171  pthsfval  30304  wlkiswwlks2lem4  30461  wlkiswwlks2lem5  30462  clwwlkvbij  30704  konigsbergumgr  30852  ex-pw  31030  ex-xp  31037  ex-rn  31041  nvvop  31211  nvm  31243  cnims  31295  ip0i  31427  ip1ilem  31428  ipdirilem  31431  ipasslem10  31441  h2hva  31576  h2hsm  31577  h2hvs  31579  axhfvadd-zf  31584  axhvcom-zf  31585  axhvass-zf  31586  axhv0cl-zf  31587  axhvaddid-zf  31588  axhfvmul-zf  31589  axhvmulid-zf  31590  axhvmulass-zf  31591  axhvdistr1-zf  31592  axhvdistr2-zf  31593  axhvmul0-zf  31594  axhfi-zf  31595  axhis1-zf  31596  axhis2-zf  31597  axhis3-zf  31598  axhis4-zf  31599  axhcompl-zf  31600  normlem0  31711  normlem1  31712  normlem2  31713  normlem4  31715  normlem9  31720  bcseqi  31722  dfhnorm2  31724  norm3difi  31749  normpari  31756  normpar2i  31758  polid2i  31759  polidi  31760  hhba  31769  hhims  31774  hhims2  31775  hhsssh  31871  hhssims  31876  hhssims2  31877  shsval3i  31990  dfch2  32009  cmcm2i  32195  fh2  32221  qlaxr3i  32238  spansnji  32248  pjcji  32286  ho0val  32352  df0op2  32354  hosd1i  32424  hosd2i  32425  eigorthi  32439  hhlnoi  32502  hhnmoi  32503  hhbloi  32504  bra0  32552  nmop0  32588  nmfn0  32589  lnopeq0lem1  32607  lnopunilem1  32612  lnophmlem2  32619  nmopcoadji  32703  pjhmopidm  32785  cvmdi  32926  cdj3lem3  33040  cdj3lem3b  33042  abrexdomjm  33103  iundifdifd  33156  iundifdif  33157  mpomptxf  33272  df1stres  33297  df2ndres  33298  intimafv  33304  fcobijfs  33313  fcobijfs2  33314  resf1o  33322  fpwrelmapffslem  33324  dpval3  33460  dp3mul10  33464  dpadd2  33476  dpmul4  33480  ccatws1f1o  33514  xrslt  33568  xrsclat  33572  xrge0tsmsd  33634  cycpmco2lem7  33693  cycpmconjv  33703  cycpmrn  33704  conjga  33731  elrgspnsubrunlem2  33809  rndrhmcl  33858  fracf1  33869  xrge0slmod  33909  lsmsnorb2  33947  qusbas2  33957  1arithidomlem2  34068  zringfrac  34086  selvply1rhm0  34158  mplvrpmga  34177  mplvrpmmhm  34178  mplvrpmrhm  34179  psrmonprod  34184  mplmonprod  34186  vieta  34212  rlmdim  34242  isconstr  34368  iconstr  34398  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  circtopn  34469  tpr2rico  34544  xrge0mulc1cn  34573  lmxrge0  34584  esumpfinvallem  34706  esumcocn  34712  hasheuni  34717  esumcvg  34718  rossros  34813  measinblem  34853  aean  34877  sxbrsigalem3  34904  dya2iocival  34905  dya2iocucvr  34916  sxbrsigalem1  34917  sxbrsigalem2  34918  sxbrsigalem5  34920  sxbrsiga  34922  fiunelcarsg  34948  eulerpartlem1  34999  eulerpartgbij  35004  fibp1  35033  coinfliplem  35111  coinflipprob  35112  ballotlemfval  35122  ballotth  35170  circlemethhgt  35272  hgt750lem2  35281  bnj1400  35465  bnj66  35490  bnj882  35556  werankwe  35739  dfscott2  35742  dfscott3  35743  derang0  35934  subfacp1lem1  35944  subfacp1lem6  35950  kur14lem7  35977  cvmsss2  36039  cvmliftlem8  36057  cvmliftlem10  36059  satfv1lem  36127  msubfval  36289  quad3  36435  bcprod  36503  bccolsum  36504  faclim  36511  pprodcnveq  36645  dfon4  36655  fobigcup  36662  dfiota3  36685  dfrecs2  36714  dfrdg4  36715  dfint3  36716  rankeq1o  36932  refssfne  37146  ssoninhaus  37236  onint1  37237  ttciun  37302  bj-dfnul2  37440  bj-rababw  37793  bj-inrab3  37842  bj-imdiridlem  38106  dissneq  38264  dffinxpf  38308  finxpreclem4  38317  rabiun  38521  ptrest  38537  poimirlem3  38541  poimirlem4  38542  poimirlem13  38551  poimirlem16  38554  poimirlem22  38560  poimirlem26  38564  poimirlem27  38565  poimirlem30  38568  cnambfre  38586  ftc1anclem8  38618  fnopabco  38657  abrexdom  38664  cncfres  38699  scottexf  39100  scott0f  39101  inres2  39179  eqrabi  39188  xpv  39194  dfres4  39231  dmxrn  39319  xrnres  39357  xrnres2  39358  rnqmap  39386  dfsucmap2  39396  dfcoss2  39435  dfcoss4  39437  1cossres  39451  dmcoss2  39476  1cosscnvxrn  39497  dfeqvrels2  39604  dfcoeleqvrels  39637  redundss3  39644  dffunsALTV5  39704  dfpeters2  39906  cdleme3d  41288  cdleme7a  41300  cdleme31sdnN  41444  cdlemk45  42004  420gcd8e4  43056  lcmeprodgcdi  43057  60lcm7e420  43060  420lcm8e840  43061  3lexlogpow5ineq1  43104  3lexlogpow2ineq1  43108  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  aks4d1p1  43126  posbezout  43150  aks6d1c1p4  43161  aks6d1c3  43173  2ap1caineq  43195  sticksstones7  43202  sticksstones12a  43207  sticksstones12  43208  aks6d1c6lem4  43223  25or6to4  43256  imaopab  43285  fmpocos  43287  dfqs3  43290  decaddcom  43341  sumcubes  43370  redvmptabs  43411  readvrec  43413  readvcot  43415  sn-00idlem2  43450  reixi  43474  sum9cubes  43683  mapfzcons  43726  eldioph4b  43817  diophren  43819  pwssplit4  44090  pwfi2f1o  44097  frlmpwfi  44099  mendplusgfval  44182  mendmulrfval  44184  mendvscafval  44187  idomodle  44192  cytpval  44203  arearect  44216  onov0suclim  44275  omabs2  44333  tr3dom  44528  har2o  44546  alephiso2  44558  alephiso3  44559  relintab  44583  dfid7  44611  cnvrcl0  44624  dfrtrcl5  44628  dfrcl3  44674  dfrcl4  44675  comptiunov2i  44705  corcltrcl  44738  neicvgnvo  45114  inductionexd  45154  mnuprdlem2  45256  nznngen  45299  hashnzfz2  45304  lhe4.4ex1a  45312  dvradcnv2  45330  binomcxplemrat  45333  binomcxplemnotnn0  45339  nregmodelf1o  46004  refsum2cnlem1  46053  fiiuncl  46081  iccdifprioo  46527  lptre2pt  46649  limclner  46660  stoweidlem13  47022  stoweidlem32  47041  stoweidlem62  47071  wallispi2lem2  47081  stirlinglem14  47096  dirkertrigeqlem1  47107  dirkercncflem4  47115  fourierdlem42  47158  fourierdlem73  47188  fourierdlem81  47196  fourierdlem92  47207  fourierdlem103  47218  fourierdlem104  47219  fouriercnp  47235  fouriersw  47240  sge0tsms  47389  sge0iunmptlemfi  47422  ovolval5lem3  47663  cnfsmf  47749  goldpolyfactor  47926  goldratval  47935  lamberte  47937  rnfdmpr  48350  fvmptrabdm  48362  fundcmpsurinjlem1  48479  m11nprm  48685  ppi1sum  48715  opoeALTV  48780  nfermltl8rev  48839  sbgoldbo  48884  evengpop3  48895  clnbgrcl  48918  clnbgrnvtx0  48924  usgrexmpl2edg  49126  usgrexmpl2nb0  49128  usgrexmpl2nb3  49131  gpg5order  49157  gpgprismgr4cycllem6  49197  cznabel  49356  cznrng  49357  mpomptx2  49446  2sphere  49860  itscnhlinecirc02plem3  49895  inlinecirc02p  49898  dftpos5  49981  tposresg  49985  icccldii  50026  dfnrm2  50039  dfnrm3  50040  elxpcbasex1ALT  50356  elxpcbasex2ALT  50358  dfswapf2  50368  swapf1a  50376  swapf1f1o  50382  swapf2f1oa  50384  swapfida  50387  setc1oterm  50598  setc1ohomfval  50600  setc1ocofval  50601  funcsetc1o  50604  dfinito4  50608  setc1onsubc  50709  islmd  50772  iscmd  50773  initocmd  50776  termolmd  50777  dvsec  50855  dvcsc  50856  dvcot  50857  amgmlemALT  50987