Theorem eqtr4i 2765

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

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  3eqtr2i  2768  3eqtr2ri  2769  3eqtr4i  2772  3eqtr4ri  2773  rabab  3461  cbvralcsf  3873  cbvrabcsf  3876  dfin5  3891  dfdif2  3892  uneqin  4217  notabw  4241  unrab  4243  inrab  4244  inrab2  4245  difrab  4246  dfrab3ss  4251  rabun2  4252  dfnul2  4264  difid  4304  rabxm  4318  elnelun  4321  abf  4334  difdifdir  4419  dfif3  4469  dfif5  4471  rabsnif  4655  tpidm  4690  ssunpr  4765  sstp  4767  opidg  4823  dfint2  4879  iunrab  4982  uniiun  4988  intiin  4989  iunid  4990  0iin  4993  mptv  5178  dfepfr  5602  epfrc  5603  xpundi  5687  xpundir  5688  csbcnv  5825  resiun2  5952  resopab  5986  mptresid  6003  dffr3  6051  dfse2  6052  cnvun  6093  imaundir  6101  imainrect  6132  cnvcnv2  6144  cnvrescnv  6146  cnvcnvres  6156  dmtpop  6169  rnsnopg  6172  resdifdi  6187  rnco2  6205  dmco  6206  co01  6213  unidmrn  6230  dfdm2  6232  predidm  6277  dfmpt3  6619  mptun  6631  funcocnv2  6792  dffv2  6922  fnasrn  7087  fpr  7097  fmptap  7114  rnmptc  7151  riotav  7318  dmoprab  7459  rnoprab2  7462  mpov  7468  mpomptx  7469  abrexex2g  7906  1stval2  7948  2ndval2  7949  fo1st  7951  fo2nd  7952  xp2  7968  dfoprab4f  7998  offval22  8027  fmpoco  8034  fimaproj  8075  tposmpo  8203  tposconst  8204  recsfval  8310  rdgsucmpt2  8359  frsucmpt2  8369  df2o3  8403  o1p1e2  8465  o2p2e4  8466  oarec  8487  omopthlem2  8586  dfqs2  8640  ecqs  8716  qliftf  8742  erovlem  8750  fset0  8791  mapsnf1o3  8833  ixp0x  8864  omf1o  9008  xpf1o  9067  mapunen  9074  enp1ilem  9178  marypha1lem  9336  marypha2lem4  9341  dfoi  9416  infeq5i  9548  oemapso  9594  cantnflem1  9601  rankelop  9789  leweon  9924  r0weon  9925  kmlem11  10074  dju1dif  10086  ackbij1lem16  10147  cf0  10164  cfsmolem  10183  alephsuc3  10494  fpwwe  10560  canthp1lem1  10566  wuncval2  10661  prlem936  10961  m1p1sr  11006  m1m1sr  11007  dfcnqs  11056  ssxr  11206  mul02lem2  11314  addrid  11317  2p2e4  12302  3p2e5  12318  3p3e6  12319  4p2e6  12320  4p3e7  12321  4p4e8  12322  5p2e7  12323  5p3e8  12324  5p4e9  12325  6p2e8  12326  6p3e9  12327  7p2e9  12328  nnzrab  12546  nn0zrab  12547  dec0u  12656  dec0h  12657  decsuc  12666  decsucc  12676  numma  12679  decma  12686  decmac  12687  decma2c  12688  decadd  12689  decaddc  12690  decmul1c  12700  decmul2c  12701  5p5e10  12706  6p4e10  12707  7p3e10  12710  8p2e10  12715  5t5e25  12738  6t6e36  12743  8t6e48  12754  nn0uz  12817  nnuz  12818  xaddcom  13183  x2times  13242  ioomax  13366  iccmax  13367  ioopos  13368  ioorp  13369  prunioo  13425  fseq1p1m1  13543  fzo13pr  13695  fzo0to2pr  13696  fzo0to3tp  13698  om2uzrdg  13909  fzennn  13921  irec  14154  sq10e99m1  14218  facnn  14228  fac0  14229  faclbnd2  14244  faclbnd4lem1  14246  hashfun  14390  hashbclem  14405  hashf1lem1  14408  hashf1lem2  14409  fz1isolem  14414  swrdccatin1  14678  swrdccat3blem  14692  s1co  14786  s2eq2s1eq  14889  s3eqs2s1eq  14891  ofs2  14924  dfid5  14980  dfid6  14981  fsumrev2  15735  fsumparts  15760  fsumiun  15775  isumnn0nn  15798  harmonic  15815  fprod2d  15937  bpoly2  16013  bpoly3  16014  bpoly4  16015  ege2le3  16046  cos1bnd  16145  efieq1re  16157  eirrlem  16162  qnnen  16171  cpnnen  16187  ruclem6  16193  3dvds  16291  pwp1fsum  16351  m1bits  16400  nn0expgcd  16524  algrp1  16534  phiprmpw  16737  prmreclem4  16881  4sqlem11  16917  4sqlem19  16925  dec5dvds  17026  decsplit1  17043  5prm  17070  7prm  17072  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  strle1  17119  grpbasex  17246  grpplusgx  17247  quslem  17498  xpsrnbas  17526  acsfn1  17618  acsfn2  17620  comfffval2  17658  dfinito2  17961  dftermo2  17962  xpchomfval  18136  xpccofval  18139  1stfval  18148  2ndfval  18151  oduleg  18247  chnub  18579  ismgmid  18624  efmndbas  18830  smndex2dnrinv  18877  grpinvfvi  18949  gaorb  19273  elcntr  19296  cntri  19298  cntrsubgnsg  19309  cntrnsg  19310  setsplusg  19316  oppgcntr  19331  gsumwrev  19332  symgressbas  19348  symgplusg  19349  symgvalstruct  19363  symgga  19373  cayleylem1  19378  psgnunilem2  19461  efgval2  19690  efgredlemc  19711  efgcpbllema  19720  frgpnabllem1  19839  gsumzaddlem  19887  gsumle  20111  opprlem  20313  oppr0  20320  opprneg  20322  rmodislmod  20920  rlmscaf  21197  xrsds  21385  gsumfsum  21409  zringunit  21441  pzriprng1  21473  cnmsgngrp  21554  psgnfix2  21574  relt  21590  ocv0  21652  thlle  21672  thlleval  21673  dsmmval2  21711  frlmip  21753  mplbas  21964  mplplusg  21981  mplmulr  21982  mplvsca2  21988  ressmplbas2  22002  ltbwe  22020  evlslem4  22052  psdmul  22154  psr1bas2  22175  ply1bas  22180  ply1assa  22184  psr1plusg  22205  psr1vsca  22206  psr1mulr  22207  ply1plusg  22208  ply1vsca  22209  ply1mulr  22210  ply1mpl0  22241  ply1mpl1  22243  coe1mul  22256  matgsum  22420  smadiadetglem1  22654  indistpsx  22993  iuncld  23028  tgrest  23142  resstopn  23169  leordtval2  23195  xkouni  23582  ptclsg  23598  ptuncnv  23790  ptunhmeo  23791  alexsubALTlem4  24033  tsmsf1o  24128  ucnimalem  24262  ressxms  24508  uniretop  24745  cnfldtopn  24764  xrtgioo  24790  zcld  24797  icccmp  24809  xrge0gsumle  24817  xrge0tsms  24818  metnrmlem3  24845  fsum2cn  24856  cnmpopc  24913  oprpiece1res1  24936  oprpiece1res2  24937  evth  24944  evth2  24945  om1opn  25021  pi1xfrf  25038  pi1xfrcnv  25042  pi1cof  25044  clsocv  25235  cncmet  25307  cnflduss  25341  rrxprds  25374  ehlbase  25400  ismbl  25511  shftmbl  25523  ioorinv  25561  itg1addlem4  25684  itg2cnlem1  25746  itg0  25765  itgss3  25800  ditgneg  25842  limcdif  25861  limciun  25879  dvexp  25938  dvef  25965  dvcnvrelem2  26003  ftc1  26027  aannenlem2  26313  dvradcnv  26404  pserdvlem2  26411  reefgim  26433  cospi  26454  sincos6thpi  26498  tanregt0  26521  dflog2  26542  logfac  26583  dvlog  26633  cxpexp  26650  cxpmul2  26671  cxpsqrt  26685  dvsqrt  26724  dvcnsqrt  26726  cxpcn2  26728  isosctrlem2  26801  1cubrlem  26823  1cubr  26824  quart1lem  26837  atancj  26892  atanlogaddlem  26895  atansopn  26914  leibpilem2  26923  log2cnv  26926  log2ublem3  26930  birthdaylem1  26933  birthdaylem2  26934  birthday  26936  dfarea  26942  lgamgulmlem5  27014  lgambdd  27018  ftalem3  27056  basellem2  27063  ppiprm  27132  ppinprm  27133  chtprm  27134  chtnprm  27135  ppi2  27151  ppi3  27152  ppiub  27185  chtub  27193  bclbnd  27261  bposlem8  27272  lgsdilem  27305  lgsdir2lem2  27307  lgsquadlem2  27362  lgsquad2lem2  27366  2lgsoddprmlem3c  27393  rplogsum  27508  mulog2sumlem2  27516  pnt2  27594  bdayfo  27659  bday0  27821  bday1  27824  old1  27875  addsasslem2  28014  negbdaylem  28066  muls01  28122  abssnid  28253  1p1e2s  28426  n0seo  28431  twocut  28433  halfcut  28468  pw2cutp1  28471  pw2cut2  28472  istrkg2ld  28546  axsegconlem9  29012  ax5seglem7  29022  iedgedg  29137  uspgrf1oedg  29260  nbgrcl  29422  nbgrnvtx0  29426  rusgrprc  29677  pthsfval  29805  wlkiswwlks2lem4  29958  wlkiswwlks2lem5  29959  clwwlkvbij  30201  konigsbergumgr  30339  ex-pw  30517  ex-xp  30524  ex-rn  30528  nvvop  30698  nvm  30730  cnims  30782  ip0i  30914  ip1ilem  30915  ipdirilem  30918  ipasslem10  30928  h2hva  31063  h2hsm  31064  h2hvs  31066  axhfvadd-zf  31071  axhvcom-zf  31072  axhvass-zf  31073  axhv0cl-zf  31074  axhvaddid-zf  31075  axhfvmul-zf  31076  axhvmulid-zf  31077  axhvmulass-zf  31078  axhvdistr1-zf  31079  axhvdistr2-zf  31080  axhvmul0-zf  31081  axhfi-zf  31082  axhis1-zf  31083  axhis2-zf  31084  axhis3-zf  31085  axhis4-zf  31086  axhcompl-zf  31087  normlem0  31198  normlem1  31199  normlem2  31200  normlem4  31202  normlem9  31207  bcseqi  31209  dfhnorm2  31211  norm3difi  31236  normpari  31243  normpar2i  31245  polid2i  31246  polidi  31247  hhba  31256  hhims  31261  hhims2  31262  hhsssh  31358  hhssims  31363  hhssims2  31364  shsval3i  31477  dfch2  31496  cmcm2i  31682  fh2  31708  qlaxr3i  31725  spansnji  31735  pjcji  31773  ho0val  31839  df0op2  31841  hosd1i  31911  hosd2i  31912  eigorthi  31926  hhlnoi  31989  hhnmoi  31990  hhbloi  31991  bra0  32039  nmop0  32075  nmfn0  32076  lnopeq0lem1  32094  lnopunilem1  32099  lnophmlem2  32106  nmopcoadji  32190  pjhmopidm  32272  cvmdi  32413  cdj3lem3  32527  cdj3lem3b  32529  abrexdomjm  32595  uniin1  32640  uniin2  32641  iundifdifd  32650  iundifdif  32651  mpomptxf  32770  df1stres  32796  df2ndres  32797  intimafv  32803  fcobijfs  32813  fcobijfs2  32814  resf1o  32822  fpwrelmapffslem  32824  sgnneg  32925  dpval3  32972  dp3mul10  32976  dpadd2  32988  dpmul4  32992  ccatws1f1o  33030  xrslt  33086  xrsclat  33090  xrge0tsmsd  33154  cycpmco2lem7  33213  cycpmconjv  33223  cycpmrn  33224  conjga  33251  elrgspnsubrunlem2  33329  rndrhmcl  33380  fracf1  33391  xrge0slmod  33431  lsmsnorb2  33475  qusbas2  33489  1arithidomlem2  33619  zringfrac  33637  selvply1rhm0  33710  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  psrmonprod  33736  mplmonprod  33738  vieta  33764  rlmdim  33794  isconstr  33920  iconstr  33950  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  circtopn  34021  tpr2rico  34096  xrge0mulc1cn  34125  lmxrge0  34136  esumpfinvallem  34258  esumcocn  34264  hasheuni  34269  esumcvg  34270  rossros  34364  measinblem  34404  aean  34428  sxbrsigalem3  34456  dya2iocival  34457  dya2iocucvr  34468  sxbrsigalem1  34469  sxbrsigalem2  34470  sxbrsigalem5  34472  sxbrsiga  34474  fiunelcarsg  34500  eulerpartlem1  34551  eulerpartgbij  34556  fibp1  34585  coinfliplem  34663  coinflipprob  34664  ballotlemfval  34674  ballotth  34722  plymulx  34732  circlemethhgt  34827  hgt750lem2  34836  bnj1400  35017  bnj66  35042  bnj882  35108  lfuhgr  35346  derang0  35397  subfacp1lem1  35407  subfacp1lem6  35413  kur14lem7  35440  cvmsss2  35502  cvmliftlem8  35520  cvmliftlem10  35522  satfv1lem  35590  msubfval  35752  quad3  35898  bcprod  35966  bccolsum  35967  faclim  35974  pprodcnveq  36109  dfon4  36119  fobigcup  36126  dfiota3  36149  dfrecs2  36178  dfrdg4  36179  dfint3  36180  rankeq1o  36399  refssfne  36586  ssoninhaus  36676  onint1  36677  ttciun  36742  bj-dfnul2  36881  bj-rababw  37234  bj-inrab3  37282  bj-imdiridlem  37545  dissneq  37703  dffinxpf  37747  finxpreclem4  37756  rabiun  37960  ptrest  37986  poimirlem3  37990  poimirlem4  37991  poimirlem13  38000  poimirlem16  38003  poimirlem22  38009  poimirlem26  38013  poimirlem27  38014  poimirlem30  38017  cnambfre  38035  ftc1anclem8  38067  fnopabco  38090  abrexdom  38097  cncfres  38132  scottexf  38535  scott0f  38536  inres2  38614  eqrabi  38623  xpv  38629  dfres4  38666  dmxrn  38754  xrnres  38792  xrnres2  38793  rnqmap  38821  dfsucmap2  38831  dfcoss2  38870  dfcoss4  38872  1cossres  38886  dmcoss2  38911  1cosscnvxrn  38932  dfeqvrels2  39039  dfcoeleqvrels  39072  redundss3  39079  dffunsALTV5  39139  dfpeters2  39341  cdleme3d  40723  cdleme7a  40735  cdleme31sdnN  40879  cdlemk45  41439  420gcd8e4  42491  lcmeprodgcdi  42492  60lcm7e420  42495  420lcm8e840  42496  3lexlogpow5ineq1  42539  3lexlogpow2ineq1  42543  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1  42561  posbezout  42585  aks6d1c1p4  42596  aks6d1c3  42608  2ap1caineq  42630  sticksstones7  42637  sticksstones12a  42642  sticksstones12  42643  aks6d1c6lem4  42658  imaopab  42718  fmpocos  42720  dfqs3  42723  decaddcom  42761  sumcubes  42790  redvmptabs  42837  readvrec  42839  readvcot  42841  sn-00idlem2  42876  reixi  42900  sum9cubes  43122  mapfzcons  43165  eldioph4b  43256  diophren  43258  pwssplit4  43534  pwfi2f1o  43541  frlmpwfi  43543  mendplusgfval  43626  mendmulrfval  43628  mendvscafval  43631  idomodle  43636  cytpval  43647  arearect  43660  onov0suclim  43719  omabs2  43777  tr3dom  43972  har2o  43990  alephiso2  44002  alephiso3  44003  relintab  44027  dfid7  44056  cnvrcl0  44069  dfrtrcl5  44073  dfrcl3  44119  dfrcl4  44120  comptiunov2i  44150  corcltrcl  44183  neicvgnvo  44559  inductionexd  44599  mnuprdlem2  44717  nznngen  44760  hashnzfz2  44765  lhe4.4ex1a  44773  dvradcnv2  44791  binomcxplemrat  44794  binomcxplemnotnn0  44800  nregmodelf1o  45459  refsum2cnlem1  45485  fiiuncl  45513  iccdifprioo  45961  lptre2pt  46083  limclner  46094  stoweidlem13  46456  stoweidlem32  46475  stoweidlem62  46505  wallispi2lem2  46515  stirlinglem14  46530  dirkertrigeqlem1  46541  dirkercncflem4  46549  fourierdlem42  46592  fourierdlem73  46622  fourierdlem81  46630  fourierdlem92  46641  fourierdlem103  46652  fourierdlem104  46653  fouriercnp  46669  fouriersw  46674  sge0tsms  46823  sge0iunmptlemfi  46856  ovolval5lem3  47097  cnfsmf  47183  nthrucw  47331  lamberte  47351  rnfdmpr  47744  fvmptrabdm  47756  fundcmpsurinjlem1  47873  m11nprm  48079  ppi1sum  48109  opoeALTV  48174  nfermltl8rev  48233  sbgoldbo  48278  evengpop3  48289  clnbgrcl  48312  clnbgrnvtx0  48318  usgrexmpl2edg  48520  usgrexmpl2nb0  48522  usgrexmpl2nb3  48525  gpg5order  48551  gpgprismgr4cycllem6  48591  cznabel  48751  cznrng  48752  mpomptx2  48826  2sphere  49240  itscnhlinecirc02plem3  49275  inlinecirc02p  49278  dftpos5  49364  tposresg  49368  icccldii  49409  dfnrm2  49422  dfnrm3  49423  elxpcbasex1ALT  49739  elxpcbasex2ALT  49741  dfswapf2  49751  swapf1a  49759  swapf1f1o  49765  swapf2f1oa  49767  swapfida  49770  setc1oterm  49981  setc1ohomfval  49983  setc1ocofval  49984  funcsetc1o  49987  dfinito4  49991  setc1onsubc  50092  islmd  50155  iscmd  50156  initocmd  50159  termolmd  50160  amgmlemALT  50293