Theorem eqtr4i 2789

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 2772	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2786	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  3eqtr2i  2792  3eqtr2ri  2793  3eqtr4i  2796  3eqtr4ri  2797  rabab  3484  cbvralcsf  3893  cbvrabcsf  3896  dfdif2  4051  dfin5  4095  uneqin  4237  notabw  4261  unrab  4263  inrab  4264  inrab2  4265  difrab  4266  dfrab3ss  4271  rabun2  4272  dfnul2  4284  difid  4328  rabxm  4343  elnelun  4346  abf  4367  difdifdir  4450  dfif3  4500  dfif5  4502  rabsnif  4686  tpidm  4721  ssunpr  4794  sstp  4796  opidg  4857  dfint2  4914  iunrab  5016  uniiun  5022  intiin  5023  iunid  5024  0iin  5027  uniin1  5038  uniin2  5039  mptv  5217  dfepfr  5642  epfrc  5643  xpundi  5727  xpundir  5728  csbcnv  5876  csbcnvOLD  5877  dmcocnv2  5976  rncocnv1  5979  resiun2  6007  resopab  6044  mptresid  6061  dffr3  6115  dfse2  6116  cnvun  6151  imaundir  6160  imainrect  6191  cnvcnv2  6203  cnvrescnv  6206  cnvcnvres  6225  dmtpop  6238  rnsnopg  6241  resdifdi  6256  rnco2  6274  dmco  6275  co01  6284  unidmrn  6306  predidm  6355  dfmpt3  6703  mptun  6715  funcocnv2OLD  6881  dffv2  7011  fnasrn  7180  fpr  7190  fmptap  7206  rnmptc  7244  riotav  7413  dmoprab  7554  rnoprab2  7557  mpov  7563  mpomptx  7564  onprcALT  7826  abrexex2g  8010  1stval2  8052  2ndval2  8053  fo1st  8055  fo2nd  8056  xp2  8072  dfoprab4f  8102  offval22  8134  fmpoco  8142  fimaproj  8189  tposmpo  8318  tposconst  8319  recsfval  8426  rdgsucmpt2  8476  frsucmpt2  8486  df2o3  8522  o1p1e2  8586  o2p2e4  8587  oarec  8608  omopthlem2  8707  dfqs2  8762  ecqs  8838  qliftf  8864  erovlem  8872  fset0  8914  mapsnf1o3  8961  ixp0x  8992  omf1o  9137  xpf1o  9196  mapunen  9203  enp1ilem  9307  marypha1lem  9462  marypha2lem4  9467  dfoi  9542  infeq5i  9674  oemapso  9720  cantnflem1  9727  rankelop  9928  leweon  10129  r0weon  10130  kmlem11  10278  dju1dif  10290  ackbij1lem16  10351  cf0  10367  cfsmolem  10387  alephsuc3  10704  fpwwe  10770  canthp1lem1  10776  wuncval2  10871  prlem936  11171  m1p1sr  11216  m1m1sr  11217  dfcnqs  11266  ssxr  11418  mul02lem2  11526  addrid  11529  2p2e4  12517  3p2e5  12533  3p3e6  12534  4p2e6  12535  4p3e7  12536  4p4e8  12537  5p2e7  12538  5p3e8  12539  5p4e9  12540  6p2e8  12541  6p3e9  12542  7p2e9  12543  nnzrab  12764  nn0zrab  12765  dec0u  12880  dec0h  12881  decsuc  12890  decsucc  12900  numma  12903  decma  12910  decmac  12911  decma2c  12912  decadd  12913  decaddc  12914  decmul1c  12924  decmul2c  12925  5p5e10  12930  6p4e10  12931  7p3e10  12934  8p2e10  12939  5t5e25  12962  6t6e36  12967  8t6e48  12978  nn0uz  13043  nnuz  13044  xaddcom  13410  x2times  13469  ioomax  13593  iccmax  13594  ioopos  13595  ioorp  13596  prunioo  13652  fseq1p1m1  13772  fzo13pr  13924  fzo0to2pr  13925  fzo0to3tp  13927  om2uzrdg  14139  fzennn  14151  irec  14385  sq10e99m1  14450  facnn  14460  fac0  14461  faclbnd2  14476  faclbnd4lem1  14478  hashfun  14623  hashbclem  14638  hashf1lem1  14641  hashf1lem2  14642  fz1isolem  14647  swrdccatin1  14916  swrdccat3blem  14930  s1co  15026  s2eq2s1eq  15130  s3eqs2s1eq  15132  ofs2  15167  dfid5  15223  dfid6  15224  sgnneg  15296  fsumrev2  15992  fsumparts  16017  fsumiun  16032  isumnn0nn  16055  harmonic  16072  fprod2d  16192  bpoly2  16267  bpoly3  16268  bpoly4  16269  ege2le3  16300  cos1bnd  16399  efieq1re  16411  eirrlem  16416  qnnen  16425  cpnnen  16441  ruclem6  16447  3dvds  16545  pwp1fsum  16605  m1bits  16654  nn0expgcd  16782  algrp1  16793  phiprmpw  16997  prmreclem4  17141  4sqlem11  17177  4sqlem19  17185  dec5dvds  17286  decsplit1  17303  5prm  17330  7prm  17332  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  strle1  17380  grpbasex  17509  grpplusgx  17510  quslem  17765  xpsrnbas  17793  acsfn1  17885  acsfn2  17887  comfffval2  17925  dfinito2  18228  dftermo2  18229  xpchomfval  18403  xpccofval  18406  1stfval  18415  2ndfval  18418  oduleg  18514  chnub  18846  idvalriota  18891  ismgmid  18895  efmndbas  19117  smndex2dnrinv  19164  degenmgmbas  19185  degenmgm2opdm  19188  grpinvfvi  19243  gaorb  19572  elcntr  19595  cntri  19597  cntrsubgnsg  19608  cntrnsg  19609  setsplusg  19615  oppgcntr  19630  gsumwrev  19631  symgressbas  19647  symgplusg  19648  symgvalstruct  19662  symgga  19672  cayleylem1  19677  psgnunilem2  19760  efgval2  19989  efgredlemc  20010  efgcpbllema  20019  frgpnabllem1  20138  gsumzaddlem  20186  gsumle  20410  opprlem  20623  oppr0  20630  opprneg  20632  rmodislmod  21256  rlmscaf  21533  xrsds  21768  gsumfsum  21794  zringunit  21827  pzriprng1  21859  cnmsgngrp  21940  psgnfix2  21960  relt  21976  ocv0  22038  thlle  22058  thlleval  22059  dsmmval2  22097  frlmip  22139  mplbas  22352  mplplusg  22369  mplmulr  22370  mplvsca2  22376  ressmplbas2  22390  ltbwe  22408  evlslem4  22440  psdmul  22542  psr1bas2  22563  ply1bas  22568  ply1assa  22572  psr1plusg  22593  psr1vsca  22594  psr1mulr  22595  ply1plusg  22596  ply1vsca  22597  ply1mulr  22598  ply1mpl0  22629  ply1mpl1  22631  coe1mul  22644  matgsum  22807  smadiadetglem1  23041  indistpsx  23383  iuncld  23418  tgrest  23532  resstopn  23559  leordtval2  23585  xkouni  23973  ptclsg  23989  ptuncnv  24181  ptunhmeo  24182  alexsubALTlem4  24424  tsmsf1o  24519  ucnimalem  24653  ressxms  24899  uniretop  25136  cnfldtopn  25155  xrtgioo  25181  zcld  25188  icccmp  25200  xrge0gsumle  25208  xrge0tsms  25209  metnrmlem3  25236  fsum2cn  25247  cnmpopc  25304  oprpiece1res1  25327  oprpiece1res2  25328  evth  25335  evth2  25336  om1opn  25412  pi1xfrf  25429  pi1xfrcnv  25433  pi1cof  25435  clsocv  25626  cncmet  25698  cnflduss  25732  rrxprds  25765  ehlbase  25791  ehl2eudis  25798  ismbl  25902  shftmbl  25914  ioorinv  25952  itg1addlem4  26075  itg2cnlem1  26137  itg0  26155  itgss3  26190  ditgneg  26232  limcdif  26251  limciun  26269  dvexp  26328  dvef  26355  dvcnvrelem2  26393  ftc1  26417  plymulidp  26658  aannenlem2  26713  dvradcnv  26805  pserdvlem2  26812  reefgim  26834  cospi  26858  sincos6thpi  26901  tanregt0  26924  dflog2  26945  logfac  26986  dvlog  27036  cxpexp  27053  cxpmul2  27074  cxpsqrt  27088  dvsqrt  27127  dvcnsqrt  27129  cxpcn2  27131  isosctrlem2  27204  1cubrlem  27226  1cubr  27227  quart1lem  27240  atancj  27295  atanlogaddlem  27298  atansopn  27317  leibpilem2  27326  log2cnv  27329  log2ublem3  27333  birthdaylem1  27336  birthdaylem2  27337  birthday  27339  dfarea  27345  lgamgulmlem5  27417  lgambdd  27421  ftalem3  27459  basellem2  27466  ppiprm  27535  ppinprm  27536  chtprm  27537  chtnprm  27538  ppi2  27554  ppi3  27555  ppiub  27588  chtub  27596  bclbnd  27664  bposlem8  27675  lgsdilem  27708  lgsdir2lem2  27710  lgsquadlem2  27765  lgsquad2lem2  27769  2lgsoddprmlem3c  27796  rplogsum  27911  mulog2sumlem2  27919  pnt2  27997  fltoprmlem2  28051  bdayfo  28091  bday0  28254  bday1  28257  old1  28308  addsasslem2  28447  negbdaylem  28499  muls01  28555  abssnid  28686  1p1e2s  28859  n0seo  28864  twocut  28866  halfcut  28901  pw2cutp1  28904  pw2cut2  28905  istrkg2ld  28979  axsegconlem9  29560  ax5seglem7  29570  iedgedg  29685  lfuhgr  29783  uspgrf1oedg  29811  nbgrcl  29973  nbgrnvtx0  29977  rusgrprc  30228  pthsfval  30361  wlkiswwlks2lem4  30518  wlkiswwlks2lem5  30519  clwwlkvbij  30761  konigsbergumgr  30909  ex-pw  31087  ex-xp  31094  ex-rn  31098  nvvop  31268  nvm  31300  cnims  31352  ip0i  31484  ip1ilem  31485  ipdirilem  31488  ipasslem10  31498  h2hva  31633  h2hsm  31634  h2hvs  31636  axhfvadd-zf  31641  axhvcom-zf  31642  axhvass-zf  31643  axhv0cl-zf  31644  axhvaddid-zf  31645  axhfvmul-zf  31646  axhvmulid-zf  31647  axhvmulass-zf  31648  axhvdistr1-zf  31649  axhvdistr2-zf  31650  axhvmul0-zf  31651  axhfi-zf  31652  axhis1-zf  31653  axhis2-zf  31654  axhis3-zf  31655  axhis4-zf  31656  axhcompl-zf  31657  normlem0  31768  normlem1  31769  normlem2  31770  normlem4  31772  normlem9  31777  bcseqi  31779  dfhnorm2  31781  norm3difi  31806  normpari  31813  normpar2i  31815  polid2i  31816  polidi  31817  hhba  31826  hhims  31831  hhims2  31832  hhsssh  31928  hhssims  31933  hhssims2  31934  shsval3i  32047  dfch2  32066  cmcm2i  32252  fh2  32278  qlaxr3i  32295  spansnji  32305  pjcji  32343  ho0val  32409  df0op2  32411  hosd1i  32481  hosd2i  32482  eigorthi  32496  hhlnoi  32559  hhnmoi  32560  hhbloi  32561  bra0  32609  nmop0  32645  nmfn0  32646  lnopeq0lem1  32664  lnopunilem1  32669  lnophmlem2  32676  nmopcoadji  32760  pjhmopidm  32842  cvmdi  32983  cdj3lem3  33097  cdj3lem3b  33099  abrexdomjm  33202  iundifdifd  33254  iundifdif  33255  mpomptxf  33369  df1stres  33394  df2ndres  33395  intimafv  33401  fcobijfs  33409  fcobijfs2  33410  resf1o  33418  fpwrelmapffslem  33420  dpval3  33556  dp3mul10  33560  dpadd2  33572  dpmul4  33576  ccatws1f1o  33610  xrslt  33667  xrsclat  33671  xrge0tsmsd  33733  cycpmco2lem7  33792  cycpmconjv  33802  cycpmrn  33803  conjga  33830  elrgspnsubrunlem2  33908  rndrhmcl  33962  fracf1  33973  xrge0slmod  34013  lsmsnorb2  34051  qusbas2  34061  1arithidomlem2  34172  zringfrac  34189  selvply1rhm0  34269  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrmonprod  34295  mplmonprod  34297  vieta  34323  rlmdim  34353  isconstr  34479  iconstr  34509  cos9thpiminplylem4  34528  cos9thpiminplylem5  34529  circtopn  34580  tpr2rico  34655  xrge0mulc1cn  34684  lmxrge0  34695  esumpfinvallem  34817  esumcocn  34823  hasheuni  34828  esumcvg  34829  rossros  34924  measinblem  34964  aean  34988  sxbrsigalem3  35015  dya2iocival  35016  dya2iocucvr  35027  sxbrsigalem1  35028  sxbrsigalem2  35029  sxbrsigalem5  35031  sxbrsiga  35033  fiunelcarsg  35059  eulerpartlem1  35110  eulerpartgbij  35115  fibp1  35144  coinfliplem  35222  coinflipprob  35223  ballotlemfval  35233  ballotth  35281  circlemethhgt  35383  hgt750lem2  35392  bnj1400  35576  bnj66  35601  bnj882  35667  onf1we  35844  werankwe  35862  werankwe2  35863  dfscott2  35867  dfscott3  35868  dfj2  36050  derang0  36142  subfacp1lem1  36152  subfacp1lem6  36158  kur14lem7  36185  cvmsss2  36247  cvmliftlem8  36265  cvmliftlem10  36267  satfv1lem  36335  msubfval  36497  quad3  36643  mirimanoff  36669  mirimanofff  36671  bcprod  36718  bccolsum  36719  faclim  36726  pprodcnveq  36860  dfon4  36870  fobigcup  36877  dfiota3  36900  dfrecs2  36929  dfrdg4  36930  dfint3  36931  rankeq1o  37147  refssfne  37361  ssoninhaus  37451  onint1  37452  ttciun  37517  bj-dfnul2  37655  bj-rababw  38008  bj-inrab3  38057  bj-cnvcnv2  38192  bj-imdiridlem  38374  dissneq  38532  dffinxpf  38576  finxpreclem4  38585  rabiun  38789  ptrest  38805  poimirlem3  38809  poimirlem4  38810  poimirlem13  38819  poimirlem16  38822  poimirlem22  38828  poimirlem26  38832  poimirlem27  38833  poimirlem30  38836  cnambfre  38854  ftc1anclem8  38886  fnopabco  38925  abrexdom  38932  cncfres  38965  scottexf  39366  scott0f  39367  inres2  39445  eqrabi  39454  xpv  39460  dfres4  39497  dmxrn  39585  xrnres  39623  xrnres2  39624  rnqmap  39652  dfsucmap2  39662  dfcoss2  39701  dfcoss4  39703  1cossres  39717  dmcoss2  39742  1cosscnvxrn  39763  dfeqvrels2  39870  dfcoeleqvrels  39903  redundss3  39910  dffunsALTV5  39970  dfpeters2  40172  cdleme3d  41554  cdleme7a  41566  cdleme31sdnN  41710  cdlemk45  42270  420gcd8e4  43322  lcmeprodgcdi  43323  60lcm7e420  43326  420lcm8e840  43327  3lexlogpow5ineq1  43370  3lexlogpow2ineq1  43374  3lexlogpow2ineq2  43375  3lexlogpow5ineq5  43376  aks4d1p1  43392  posbezout  43416  aks6d1c1p4  43427  aks6d1c3  43439  2ap1caineq  43461  sticksstones7  43468  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem4  43489  25or6to4  43522  imaopab  43552  fmpocos  43554  dfqs3  43557  decaddcom  43607  sumcubes  43636  redvmptabs  43677  readvrec  43679  readvcot  43681  sn-00idlem2  43716  reixi  43740  sum9cubes  43949  mapfzcons  43993  eldioph4b  44084  diophren  44086  pwssplit4  44357  pwfi2f1o  44364  frlmpwfi  44366  mendplusgfval  44444  mendmulrfval  44446  mendvscafval  44449  idomodle  44454  cytpval  44465  arearect  44478  onov0suclim  44537  omabs2  44595  tr3dom  44790  har2o  44808  alephiso2  44820  alephiso3  44821  relintab  44845  dfid7  44873  cnvrcl0  44886  dfrtrcl5  44890  dfrcl3  44936  dfrcl4  44937  comptiunov2i  44967  corcltrcl  45000  neicvgnvo  45376  inductionexd  45416  mnuprdlem2  45518  nznngen  45561  hashnzfz2  45566  lhe4.4ex1a  45574  dvradcnv2  45592  binomcxplemrat  45595  binomcxplemnotnn0  45601  nregmodelf1o  46269  refsum2cnlem1  46328  fiiuncl  46356  iccdifprioo  46801  lptre2pt  46923  limclner  46934  stoweidlem13  47296  stoweidlem32  47315  stoweidlem62  47345  wallispi2lem2  47355  stirlinglem14  47370  dirkertrigeqlem1  47381  dirkercncflem4  47389  fourierdlem42  47432  fourierdlem73  47462  fourierdlem81  47470  fourierdlem92  47481  fourierdlem103  47492  fourierdlem104  47493  fouriercnp  47509  fouriersw  47514  sge0tsms  47663  sge0iunmptlemfi  47696  ovolval5lem3  47937  cnfsmf  48023  goldpolyfactor  48200  goldratval  48209  lamberte  48211  rnfdmpr  48624  fvmptrabdm  48636  fundcmpsurinjlem1  48753  m11nprm  48959  ppi1sum  48989  opoeALTV  49054  nfermltl8rev  49113  sbgoldbo  49158  evengpop3  49169  clnbgrcl  49192  clnbgrnvtx0  49198  usgrexmpl2edg  49400  usgrexmpl2nb0  49402  usgrexmpl2nb3  49405  gpg5order  49431  gpgprismgr4cycllem6  49471  cznabel  49630  cznrng  49631  subrgccdom  49709  bru3val  49753  mpomptx2  49778  dftpos5  50318  tposresg  50322  icccldii  50364  dfnrm2  50377  dfnrm3  50378  elxpcbasex1ALT  50702  elxpcbasex2ALT  50704  dfswapf2  50714  swapf1a  50722  swapf1f1o  50728  swapf2f1oa  50730  swapfida  50733  setc1oterm  50957  setc1ohomfval  50959  setc1ocofval  50960  funcsetc1o  50963  dfinito4  50967  setc1onsubc  51071  islmd  51179  iscmd  51180  initocmd  51183  termolmd  51184  dvsec  51284  dvcsc  51285  dvcot  51286  amgmlemALT  51416