Theorem eqtr4i 2762

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  3eqtr2i  2765  3eqtr2ri  2766  3eqtr4i  2769  3eqtr4ri  2770  rabab  3460  cbvralcsf  3879  cbvrabcsf  3882  dfin5  3897  dfdif2  3898  uneqin  4229  notabw  4253  unrab  4255  inrab  4256  inrab2  4257  difrab  4258  dfrab3ss  4263  rabun2  4264  dfnul2  4276  difid  4316  rabxm  4330  elnelun  4333  abf  4346  difdifdir  4431  dfif3  4481  dfif5  4483  rabsnif  4667  tpidm  4702  ssunpr  4777  sstp  4779  opidg  4835  dfint2  4891  iunrab  4995  uniiun  5001  intiin  5002  iunid  5003  0iin  5006  mptv  5191  dfepfr  5615  epfrc  5616  xpundi  5700  xpundir  5701  csbcnv  5838  resiun2  5965  resopab  5999  mptresid  6016  dffr3  6064  dfse2  6065  cnvun  6106  imaundir  6114  imainrect  6145  cnvcnv2  6157  cnvrescnv  6159  cnvcnvres  6169  dmtpop  6182  rnsnopg  6185  resdifdi  6200  rnco2  6218  dmco  6219  co01  6226  unidmrn  6243  dfdm2  6245  predidm  6290  dfmpt3  6632  mptun  6644  funcocnv2  6805  dffv2  6935  fnasrn  7098  fpr  7108  fmptap  7125  rnmptc  7162  riotav  7329  dmoprab  7470  rnoprab2  7473  mpov  7479  mpomptx  7480  abrexex2g  7917  1stval2  7959  2ndval2  7960  fo1st  7962  fo2nd  7963  xp2  7979  dfoprab4f  8009  offval22  8038  fmpoco  8045  fimaproj  8085  tposmpo  8213  tposconst  8214  recsfval  8320  rdgsucmpt2  8369  frsucmpt2  8379  df2o3  8413  o1p1e2  8475  o2p2e4  8476  oarec  8497  omopthlem2  8596  dfqs2  8650  ecqs  8726  qliftf  8752  erovlem  8760  fset0  8801  mapsnf1o3  8843  ixp0x  8874  omf1o  9018  xpf1o  9077  mapunen  9084  enp1ilem  9188  marypha1lem  9346  marypha2lem4  9351  dfoi  9426  infeq5i  9557  oemapso  9603  cantnflem1  9610  rankelop  9798  leweon  9933  r0weon  9934  kmlem11  10083  dju1dif  10095  ackbij1lem16  10156  cf0  10173  cfsmolem  10192  alephsuc3  10503  fpwwe  10569  canthp1lem1  10575  wuncval2  10670  prlem936  10970  m1p1sr  11015  m1m1sr  11016  dfcnqs  11065  ssxr  11215  mul02lem2  11323  addrid  11326  2p2e4  12311  3p2e5  12327  3p3e6  12328  4p2e6  12329  4p3e7  12330  4p4e8  12331  5p2e7  12332  5p3e8  12333  5p4e9  12334  6p2e8  12335  6p3e9  12336  7p2e9  12337  nnzrab  12555  nn0zrab  12556  dec0u  12665  dec0h  12666  decsuc  12675  decsucc  12685  numma  12688  decma  12695  decmac  12696  decma2c  12697  decadd  12698  decaddc  12699  decmul1c  12709  decmul2c  12710  5p5e10  12715  6p4e10  12716  7p3e10  12719  8p2e10  12724  5t5e25  12747  6t6e36  12752  8t6e48  12763  nn0uz  12826  nnuz  12827  xaddcom  13192  x2times  13251  ioomax  13375  iccmax  13376  ioopos  13377  ioorp  13378  prunioo  13434  fseq1p1m1  13552  fzo13pr  13704  fzo0to2pr  13705  fzo0to3tp  13707  om2uzrdg  13918  fzennn  13930  irec  14163  sq10e99m1  14227  facnn  14237  fac0  14238  faclbnd2  14253  faclbnd4lem1  14255  hashfun  14399  hashbclem  14414  hashf1lem1  14417  hashf1lem2  14418  fz1isolem  14423  swrdccatin1  14687  swrdccat3blem  14701  s1co  14795  s2eq2s1eq  14898  s3eqs2s1eq  14900  ofs2  14933  dfid5  14989  dfid6  14990  fsumrev2  15744  fsumparts  15769  fsumiun  15784  isumnn0nn  15807  harmonic  15824  fprod2d  15946  bpoly2  16022  bpoly3  16023  bpoly4  16024  ege2le3  16055  cos1bnd  16154  efieq1re  16166  eirrlem  16171  qnnen  16180  cpnnen  16196  ruclem6  16202  3dvds  16300  pwp1fsum  16360  m1bits  16409  nn0expgcd  16533  algrp1  16543  phiprmpw  16746  prmreclem4  16890  4sqlem11  16926  4sqlem19  16934  dec5dvds  17035  decsplit1  17052  5prm  17079  7prm  17081  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  strle1  17128  grpbasex  17255  grpplusgx  17256  quslem  17507  xpsrnbas  17535  acsfn1  17627  acsfn2  17629  comfffval2  17667  dfinito2  17970  dftermo2  17971  xpchomfval  18145  xpccofval  18148  1stfval  18157  2ndfval  18160  oduleg  18256  chnub  18588  ismgmid  18633  efmndbas  18839  smndex2dnrinv  18886  grpinvfvi  18958  gaorb  19282  elcntr  19305  cntri  19307  cntrsubgnsg  19318  cntrnsg  19319  setsplusg  19325  oppgcntr  19340  gsumwrev  19341  symgressbas  19357  symgplusg  19358  symgvalstruct  19372  symgga  19382  cayleylem1  19387  psgnunilem2  19470  efgval2  19699  efgredlemc  19720  efgcpbllema  19729  frgpnabllem1  19848  gsumzaddlem  19896  gsumle  20120  opprlem  20322  oppr0  20329  opprneg  20331  rmodislmod  20925  rlmscaf  21202  xrsds  21390  gsumfsum  21414  zringunit  21446  pzriprng1  21478  cnmsgngrp  21559  psgnfix2  21579  relt  21595  ocv0  21657  thlle  21677  thlleval  21678  dsmmval2  21716  frlmip  21758  mplbas  21968  mplplusg  21985  mplmulr  21986  mplvsca2  21992  ressmplbas2  22005  ltbwe  22022  evlslem4  22054  psdmul  22132  psr1bas2  22153  ply1bas  22158  ply1basOLD  22159  ply1assa  22163  psr1plusg  22184  psr1vsca  22185  psr1mulr  22186  ply1plusg  22187  ply1vsca  22188  ply1mulr  22189  ply1mpl0  22220  ply1mpl1  22222  coe1mul  22235  matgsum  22402  smadiadetglem1  22636  indistpsx  22975  iuncld  23010  tgrest  23124  resstopn  23151  leordtval2  23177  xkouni  23564  ptclsg  23580  ptuncnv  23772  ptunhmeo  23773  alexsubALTlem4  24015  tsmsf1o  24110  ucnimalem  24244  ressxms  24490  uniretop  24727  cnfldtopn  24746  xrtgioo  24772  zcld  24779  icccmp  24791  xrge0gsumle  24799  xrge0tsms  24800  metnrmlem3  24827  fsum2cn  24838  cnmpopc  24895  oprpiece1res1  24918  oprpiece1res2  24919  evth  24926  evth2  24927  om1opn  25003  pi1xfrf  25020  pi1xfrcnv  25024  pi1cof  25026  clsocv  25217  cncmet  25289  cnflduss  25323  rrxprds  25356  ehlbase  25382  ismbl  25493  shftmbl  25505  ioorinv  25543  itg1addlem4  25666  itg2cnlem1  25728  itg0  25747  itgss3  25782  ditgneg  25824  limcdif  25843  limciun  25861  dvexp  25920  dvef  25947  dvcnvrelem2  25985  ftc1  26009  aannenlem2  26295  dvradcnv  26386  pserdvlem2  26393  reefgim  26415  cospi  26436  sincos6thpi  26480  tanregt0  26503  dflog2  26524  logfac  26565  dvlog  26615  cxpexp  26632  cxpmul2  26653  cxpsqrt  26667  dvsqrt  26706  dvcnsqrt  26708  cxpcn2  26710  isosctrlem2  26783  1cubrlem  26805  1cubr  26806  quart1lem  26819  atancj  26874  atanlogaddlem  26877  atansopn  26896  leibpilem2  26905  log2cnv  26908  log2ublem3  26912  birthdaylem1  26915  birthdaylem2  26916  birthday  26918  dfarea  26924  lgamgulmlem5  26996  lgambdd  27000  ftalem3  27038  basellem2  27045  ppiprm  27114  ppinprm  27115  chtprm  27116  chtnprm  27117  ppi2  27133  ppi3  27134  ppiub  27167  chtub  27175  bclbnd  27243  bposlem8  27254  lgsdilem  27287  lgsdir2lem2  27289  lgsquadlem2  27344  lgsquad2lem2  27348  2lgsoddprmlem3c  27375  rplogsum  27490  mulog2sumlem2  27498  pnt2  27576  bdayfo  27641  bday0  27803  bday1  27806  old1  27857  addsasslem2  27996  negbdaylem  28048  muls01  28104  abssnid  28235  1p1e2s  28408  n0seo  28413  twocut  28415  halfcut  28450  pw2cutp1  28453  pw2cut2  28454  istrkg2ld  28528  axsegconlem9  28994  ax5seglem7  29004  iedgedg  29119  uspgrf1oedg  29242  nbgrcl  29404  nbgrnvtx0  29408  rusgrprc  29659  pthsfval  29787  wlkiswwlks2lem4  29940  wlkiswwlks2lem5  29941  clwwlkvbij  30183  konigsbergumgr  30321  ex-pw  30499  ex-xp  30506  ex-rn  30510  nvvop  30680  nvm  30712  cnims  30764  ip0i  30896  ip1ilem  30897  ipdirilem  30900  ipasslem10  30910  h2hva  31045  h2hsm  31046  h2hvs  31048  axhfvadd-zf  31053  axhvcom-zf  31054  axhvass-zf  31055  axhv0cl-zf  31056  axhvaddid-zf  31057  axhfvmul-zf  31058  axhvmulid-zf  31059  axhvmulass-zf  31060  axhvdistr1-zf  31061  axhvdistr2-zf  31062  axhvmul0-zf  31063  axhfi-zf  31064  axhis1-zf  31065  axhis2-zf  31066  axhis3-zf  31067  axhis4-zf  31068  axhcompl-zf  31069  normlem0  31180  normlem1  31181  normlem2  31182  normlem4  31184  normlem9  31189  bcseqi  31191  dfhnorm2  31193  norm3difi  31218  normpari  31225  normpar2i  31227  polid2i  31228  polidi  31229  hhba  31238  hhims  31243  hhims2  31244  hhsssh  31340  hhssims  31345  hhssims2  31346  shsval3i  31459  dfch2  31478  cmcm2i  31664  fh2  31690  qlaxr3i  31707  spansnji  31717  pjcji  31755  ho0val  31821  df0op2  31823  hosd1i  31893  hosd2i  31894  eigorthi  31908  hhlnoi  31971  hhnmoi  31972  hhbloi  31973  bra0  32021  nmop0  32057  nmfn0  32058  lnopeq0lem1  32076  lnopunilem1  32081  lnophmlem2  32088  nmopcoadji  32172  pjhmopidm  32254  cvmdi  32395  cdj3lem3  32509  cdj3lem3b  32511  abrexdomjm  32577  uniin1  32621  uniin2  32622  iundifdifd  32631  iundifdif  32632  mpomptxf  32751  df1stres  32777  df2ndres  32778  intimafv  32784  fcobijfs  32794  fcobijfs2  32795  resf1o  32803  fpwrelmapffslem  32805  sgnneg  32906  dpval3  32953  dp3mul10  32957  dpadd2  32969  dpmul4  32973  ccatws1f1o  33011  xrslt  33067  xrsclat  33071  xrge0tsmsd  33134  cycpmco2lem7  33193  cycpmconjv  33203  cycpmrn  33204  conjga  33231  elrgspnsubrunlem2  33309  rndrhmcl  33357  fracf1  33368  xrge0slmod  33408  lsmsnorb2  33452  qusbas2  33466  1arithidomlem2  33596  zringfrac  33614  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonprod  33696  mplmonprod  33698  vieta  33724  rlmdim  33754  isconstr  33880  iconstr  33910  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  circtopn  33981  tpr2rico  34056  xrge0mulc1cn  34085  lmxrge0  34096  esumpfinvallem  34218  esumcocn  34224  hasheuni  34229  esumcvg  34230  rossros  34324  measinblem  34364  aean  34388  sxbrsigalem3  34416  dya2iocival  34417  dya2iocucvr  34428  sxbrsigalem1  34429  sxbrsigalem2  34430  sxbrsigalem5  34432  sxbrsiga  34434  fiunelcarsg  34460  eulerpartlem1  34511  eulerpartgbij  34516  fibp1  34545  coinfliplem  34623  coinflipprob  34624  ballotlemfval  34634  ballotth  34682  plymulx  34692  circlemethhgt  34787  hgt750lem2  34796  bnj1400  34977  bnj66  35002  bnj882  35068  lfuhgr  35300  derang0  35351  subfacp1lem1  35361  subfacp1lem6  35367  kur14lem7  35394  cvmsss2  35456  cvmliftlem8  35474  cvmliftlem10  35476  satfv1lem  35544  msubfval  35706  quad3  35852  bcprod  35920  bccolsum  35921  faclim  35928  pprodcnveq  36063  dfon4  36073  fobigcup  36080  dfiota3  36103  dfrecs2  36132  dfrdg4  36133  dfint3  36134  rankeq1o  36353  refssfne  36540  ssoninhaus  36630  onint1  36631  ttciun  36696  bj-dfnul2  36835  bj-rababw  37188  bj-inrab3  37236  bj-imdiridlem  37499  dissneq  37657  dffinxpf  37701  finxpreclem4  37710  rabiun  37914  ptrest  37940  poimirlem3  37944  poimirlem4  37945  poimirlem13  37954  poimirlem16  37957  poimirlem22  37963  poimirlem26  37967  poimirlem27  37968  poimirlem30  37971  cnambfre  37989  ftc1anclem8  38021  fnopabco  38044  abrexdom  38051  cncfres  38086  scottexf  38489  scott0f  38490  inres2  38568  eqrabi  38577  xpv  38583  dfres4  38620  dmxrn  38708  xrnres  38746  xrnres2  38747  rnqmap  38775  dfsucmap2  38785  dfcoss2  38824  dfcoss4  38826  1cossres  38840  dmcoss2  38865  1cosscnvxrn  38886  dfeqvrels2  38993  dfcoeleqvrels  39026  redundss3  39033  dffunsALTV5  39093  dfpeters2  39295  cdleme3d  40677  cdleme7a  40689  cdleme31sdnN  40833  cdlemk45  41393  420gcd8e4  42445  lcmeprodgcdi  42446  60lcm7e420  42449  420lcm8e840  42450  3lexlogpow5ineq1  42493  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1p1  42515  posbezout  42539  aks6d1c1p4  42550  aks6d1c3  42562  2ap1caineq  42584  sticksstones7  42591  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem4  42612  imaopab  42672  fmpocos  42675  dfqs3  42678  decaddcom  42716  sumcubes  42745  redvmptabs  42792  readvrec  42794  readvcot  42796  sn-00idlem2  42831  reixi  42855  sum9cubes  43105  mapfzcons  43148  eldioph4b  43239  diophren  43241  pwssplit4  43517  pwfi2f1o  43524  frlmpwfi  43526  mendplusgfval  43609  mendmulrfval  43611  mendvscafval  43614  idomodle  43619  cytpval  43630  arearect  43643  onov0suclim  43702  omabs2  43760  tr3dom  43955  har2o  43973  alephiso2  43985  alephiso3  43986  relintab  44010  dfid7  44039  cnvrcl0  44052  dfrtrcl5  44056  dfrcl3  44102  dfrcl4  44103  comptiunov2i  44133  corcltrcl  44166  neicvgnvo  44542  inductionexd  44582  mnuprdlem2  44700  nznngen  44743  hashnzfz2  44748  lhe4.4ex1a  44756  dvradcnv2  44774  binomcxplemrat  44777  binomcxplemnotnn0  44783  nregmodelf1o  45442  refsum2cnlem1  45468  fiiuncl  45496  iccdifprioo  45946  lptre2pt  46068  limclner  46079  stoweidlem13  46441  stoweidlem32  46460  stoweidlem62  46490  wallispi2lem2  46500  stirlinglem14  46515  dirkertrigeqlem1  46526  dirkercncflem4  46534  fourierdlem42  46577  fourierdlem73  46607  fourierdlem81  46615  fourierdlem92  46626  fourierdlem103  46637  fourierdlem104  46638  fouriercnp  46654  fouriersw  46659  sge0tsms  46808  sge0iunmptlemfi  46841  ovolval5lem3  47082  cnfsmf  47168  nthrucw  47316  lamberte  47336  rnfdmpr  47729  fvmptrabdm  47741  fundcmpsurinjlem1  47858  m11nprm  48064  ppi1sum  48094  opoeALTV  48159  nfermltl8rev  48218  sbgoldbo  48263  evengpop3  48274  clnbgrcl  48297  clnbgrnvtx0  48303  usgrexmpl2edg  48505  usgrexmpl2nb0  48507  usgrexmpl2nb3  48510  gpg5order  48536  gpgprismgr4cycllem6  48576  cznabel  48736  cznrng  48737  mpomptx2  48811  2sphere  49225  itscnhlinecirc02plem3  49260  inlinecirc02p  49263  dftpos5  49349  tposresg  49353  icccldii  49394  dfnrm2  49407  dfnrm3  49408  elxpcbasex1ALT  49724  elxpcbasex2ALT  49726  dfswapf2  49736  swapf1a  49744  swapf1f1o  49750  swapf2f1oa  49752  swapfida  49755  setc1oterm  49966  setc1ohomfval  49968  setc1ocofval  49969  funcsetc1o  49972  dfinito4  49976  setc1onsubc  50077  islmd  50140  iscmd  50141  initocmd  50144  termolmd  50145  amgmlemALT  50278