Theorem eqtr4i 2788

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  3eqtr2i  2791  3eqtr2ri  2792  3eqtr4i  2795  3eqtr4ri  2796  rabab  3484  cbvralcsf  3894  cbvrabcsf  3897  dfin5  3912  dfdif2  3913  uneqin  4241  notabw  4265  unrab  4267  inrab  4268  inrab2  4269  difrab  4270  dfrab3ss  4275  rabun2  4276  dfnul2  4288  difid  4329  rabxm  4344  elnelun  4347  abf  4360  difdifdir  4445  dfif3  4495  dfif5  4497  rabsnif  4682  tpidm  4717  ssunpr  4792  sstp  4794  opidg  4850  dfint2  4907  iunrab  5010  uniiun  5016  intiin  5017  iunid  5018  0iin  5021  mptv  5206  dfepfr  5631  epfrc  5632  xpundi  5716  xpundir  5717  csbcnv  5858  csbcnvOLD  5859  resiun2  5986  resopab  6023  mptresid  6040  dffr3  6088  dfse2  6089  cnvun  6126  imaundir  6135  imainrect  6167  cnvcnv2  6179  cnvrescnv  6182  cnvcnvres  6192  dmtpop  6205  rnsnopg  6208  resdifdi  6223  rnco2  6241  dmco  6242  co01  6249  unidmrn  6266  dfdm2  6268  predidm  6313  dfmpt3  6655  mptun  6667  funcocnv2  6832  dffv2  6962  fnasrn  7127  fpr  7137  fmptap  7154  rnmptc  7191  riotav  7358  dmoprab  7499  rnoprab2  7502  mpov  7508  mpomptx  7509  abrexex2g  7945  1stval2  7987  2ndval2  7988  fo1st  7990  fo2nd  7991  xp2  8007  dfoprab4f  8037  offval22  8067  fmpoco  8074  fimaproj  8115  tposmpo  8243  tposconst  8244  recsfval  8351  rdgsucmpt2  8401  frsucmpt2  8411  df2o3  8445  o1p1e2  8509  o2p2e4  8510  oarec  8531  omopthlem2  8630  dfqs2  8685  ecqs  8761  qliftf  8787  erovlem  8795  fset0  8835  mapsnf1o3  8877  ixp0x  8908  omf1o  9052  xpf1o  9111  mapunen  9118  enp1ilem  9222  marypha1lem  9379  marypha2lem4  9384  dfoi  9459  infeq5i  9591  oemapso  9637  cantnflem1  9644  rankelop  9832  leweon  9967  r0weon  9968  kmlem11  10117  dju1dif  10129  ackbij1lem16  10190  cf0  10207  cfsmolem  10227  alephsuc3  10538  fpwwe  10604  canthp1lem1  10610  wuncval2  10705  prlem936  11005  m1p1sr  11050  m1m1sr  11051  dfcnqs  11100  ssxr  11252  mul02lem2  11360  addrid  11363  2p2e4  12352  3p2e5  12368  3p3e6  12369  4p2e6  12370  4p3e7  12371  4p4e8  12372  5p2e7  12373  5p3e8  12374  5p4e9  12375  6p2e8  12376  6p3e9  12377  7p2e9  12378  nnzrab  12599  nn0zrab  12600  dec0u  12714  dec0h  12715  decsuc  12724  decsucc  12734  numma  12737  decma  12744  decmac  12745  decma2c  12746  decadd  12747  decaddc  12748  decmul1c  12758  decmul2c  12759  5p5e10  12764  6p4e10  12765  7p3e10  12768  8p2e10  12773  5t5e25  12796  6t6e36  12801  8t6e48  12812  nn0uz  12877  nnuz  12878  xaddcom  13243  x2times  13302  ioomax  13426  iccmax  13427  ioopos  13428  ioorp  13429  prunioo  13485  fseq1p1m1  13603  fzo13pr  13755  fzo0to2pr  13756  fzo0to3tp  13758  om2uzrdg  13969  fzennn  13981  irec  14214  sq10e99m1  14278  facnn  14288  fac0  14289  faclbnd2  14304  faclbnd4lem1  14306  hashfun  14450  hashbclem  14465  hashf1lem1  14468  hashf1lem2  14469  fz1isolem  14474  swrdccatin1  14738  swrdccat3blem  14752  s1co  14846  s2eq2s1eq  14949  s3eqs2s1eq  14951  ofs2  14984  dfid5  15040  dfid6  15041  sgnneg  15113  fsumrev2  15809  fsumparts  15834  fsumiun  15849  isumnn0nn  15872  harmonic  15889  fprod2d  16011  bpoly2  16087  bpoly3  16088  bpoly4  16089  ege2le3  16120  cos1bnd  16219  efieq1re  16231  eirrlem  16236  qnnen  16245  cpnnen  16261  ruclem6  16267  3dvds  16365  pwp1fsum  16425  m1bits  16474  nn0expgcd  16598  algrp1  16608  phiprmpw  16811  prmreclem4  16955  4sqlem11  16991  4sqlem19  16999  dec5dvds  17100  decsplit1  17117  5prm  17144  7prm  17146  1259lem2  17168  1259lem3  17169  1259lem4  17170  1259lem5  17171  1259prm  17172  2503lem1  17173  2503lem2  17174  2503lem3  17175  2503prm  17176  4001lem1  17177  4001lem2  17178  4001lem3  17179  4001lem4  17180  4001prm  17181  strle1  17194  grpbasex  17321  grpplusgx  17322  quslem  17573  xpsrnbas  17601  acsfn1  17693  acsfn2  17695  comfffval2  17733  dfinito2  18036  dftermo2  18037  xpchomfval  18211  xpccofval  18214  1stfval  18223  2ndfval  18226  oduleg  18322  chnub  18654  ismgmid  18699  efmndbas  18905  smndex2dnrinv  18952  grpinvfvi  19024  gaorb  19347  elcntr  19370  cntri  19372  cntrsubgnsg  19383  cntrnsg  19384  setsplusg  19390  oppgcntr  19405  gsumwrev  19406  symgressbas  19422  symgplusg  19423  symgvalstruct  19437  symgga  19447  cayleylem1  19452  psgnunilem2  19535  efgval2  19764  efgredlemc  19785  efgcpbllema  19794  frgpnabllem1  19913  gsumzaddlem  19961  gsumle  20185  opprlem  20391  oppr0  20398  opprneg  20400  rmodislmod  20997  rlmscaf  21274  xrsds  21462  gsumfsum  21486  zringunit  21518  pzriprng1  21550  cnmsgngrp  21631  psgnfix2  21651  relt  21667  ocv0  21729  thlle  21749  thlleval  21750  dsmmval2  21788  frlmip  21830  mplbas  22041  mplplusg  22058  mplmulr  22059  mplvsca2  22065  ressmplbas2  22079  ltbwe  22097  evlslem4  22129  psdmul  22231  psr1bas2  22252  ply1bas  22257  ply1assa  22261  psr1plusg  22282  psr1vsca  22283  psr1mulr  22284  ply1plusg  22285  ply1vsca  22286  ply1mulr  22287  ply1mpl0  22318  ply1mpl1  22320  coe1mul  22333  matgsum  22497  smadiadetglem1  22731  indistpsx  23070  iuncld  23105  tgrest  23219  resstopn  23246  leordtval2  23272  xkouni  23659  ptclsg  23675  ptuncnv  23867  ptunhmeo  23868  alexsubALTlem4  24110  tsmsf1o  24205  ucnimalem  24339  ressxms  24585  uniretop  24822  cnfldtopn  24841  xrtgioo  24867  zcld  24874  icccmp  24886  xrge0gsumle  24894  xrge0tsms  24895  metnrmlem3  24922  fsum2cn  24933  cnmpopc  24990  oprpiece1res1  25013  oprpiece1res2  25014  evth  25021  evth2  25022  om1opn  25098  pi1xfrf  25115  pi1xfrcnv  25119  pi1cof  25121  clsocv  25312  cncmet  25384  cnflduss  25418  rrxprds  25451  ehlbase  25477  ismbl  25588  shftmbl  25600  ioorinv  25638  itg1addlem4  25761  itg2cnlem1  25823  itg0  25842  itgss3  25877  ditgneg  25919  limcdif  25938  limciun  25956  dvexp  26015  dvef  26042  dvcnvrelem2  26080  ftc1  26104  plymulidp  26346  aannenlem2  26393  dvradcnv  26484  pserdvlem2  26491  reefgim  26513  cospi  26537  sincos6thpi  26581  tanregt0  26604  dflog2  26625  logfac  26666  dvlog  26716  cxpexp  26733  cxpmul2  26754  cxpsqrt  26768  dvsqrt  26807  dvcnsqrt  26809  cxpcn2  26811  isosctrlem2  26884  1cubrlem  26906  1cubr  26907  quart1lem  26920  atancj  26975  atanlogaddlem  26978  atansopn  26997  leibpilem2  27006  log2cnv  27009  log2ublem3  27013  birthdaylem1  27016  birthdaylem2  27017  birthday  27019  dfarea  27025  lgamgulmlem5  27097  lgambdd  27101  ftalem3  27139  basellem2  27146  ppiprm  27215  ppinprm  27216  chtprm  27217  chtnprm  27218  ppi2  27234  ppi3  27235  ppiub  27268  chtub  27276  bclbnd  27344  bposlem8  27355  lgsdilem  27388  lgsdir2lem2  27390  lgsquadlem2  27445  lgsquad2lem2  27449  2lgsoddprmlem3c  27476  rplogsum  27591  mulog2sumlem2  27599  pnt2  27677  bdayfo  27741  bday0  27904  bday1  27907  old1  27958  addsasslem2  28097  negbdaylem  28149  muls01  28205  abssnid  28336  1p1e2s  28509  n0seo  28514  twocut  28516  halfcut  28551  pw2cutp1  28554  pw2cut2  28555  istrkg2ld  28629  axsegconlem9  29126  ax5seglem7  29136  iedgedg  29251  uspgrf1oedg  29374  nbgrcl  29536  nbgrnvtx0  29540  rusgrprc  29791  pthsfval  29919  wlkiswwlks2lem4  30072  wlkiswwlks2lem5  30073  clwwlkvbij  30315  konigsbergumgr  30453  ex-pw  30631  ex-xp  30638  ex-rn  30642  nvvop  30812  nvm  30844  cnims  30896  ip0i  31028  ip1ilem  31029  ipdirilem  31032  ipasslem10  31042  h2hva  31177  h2hsm  31178  h2hvs  31180  axhfvadd-zf  31185  axhvcom-zf  31186  axhvass-zf  31187  axhv0cl-zf  31188  axhvaddid-zf  31189  axhfvmul-zf  31190  axhvmulid-zf  31191  axhvmulass-zf  31192  axhvdistr1-zf  31193  axhvdistr2-zf  31194  axhvmul0-zf  31195  axhfi-zf  31196  axhis1-zf  31197  axhis2-zf  31198  axhis3-zf  31199  axhis4-zf  31200  axhcompl-zf  31201  normlem0  31312  normlem1  31313  normlem2  31314  normlem4  31316  normlem9  31321  bcseqi  31323  dfhnorm2  31325  norm3difi  31350  normpari  31357  normpar2i  31359  polid2i  31360  polidi  31361  hhba  31370  hhims  31375  hhims2  31376  hhsssh  31472  hhssims  31477  hhssims2  31478  shsval3i  31591  dfch2  31610  cmcm2i  31796  fh2  31822  qlaxr3i  31839  spansnji  31849  pjcji  31887  ho0val  31953  df0op2  31955  hosd1i  32025  hosd2i  32026  eigorthi  32040  hhlnoi  32103  hhnmoi  32104  hhbloi  32105  bra0  32153  nmop0  32189  nmfn0  32190  lnopeq0lem1  32208  lnopunilem1  32213  lnophmlem2  32220  nmopcoadji  32304  pjhmopidm  32386  cvmdi  32527  cdj3lem3  32641  cdj3lem3b  32643  abrexdomjm  32706  uniin1  32751  uniin2  32752  iundifdifd  32761  iundifdif  32762  mpomptxf  32880  df1stres  32906  df2ndres  32907  intimafv  32913  fcobijfs  32923  fcobijfs2  32924  resf1o  32932  fpwrelmapffslem  32934  dpval3  33071  dp3mul10  33075  dpadd2  33087  dpmul4  33091  ccatws1f1o  33129  xrslt  33185  xrsclat  33189  xrge0tsmsd  33253  cycpmco2lem7  33312  cycpmconjv  33322  cycpmrn  33323  conjga  33350  elrgspnsubrunlem2  33429  rndrhmcl  33483  fracf1  33494  xrge0slmod  33534  lsmsnorb2  33578  qusbas2  33592  1arithidomlem2  33732  zringfrac  33750  selvply1rhm0  33823  mplvrpmga  33842  mplvrpmmhm  33843  mplvrpmrhm  33844  psrmonprod  33849  mplmonprod  33851  vieta  33877  rlmdim  33907  isconstr  34033  iconstr  34063  cos9thpiminplylem4  34082  cos9thpiminplylem5  34083  circtopn  34134  tpr2rico  34209  xrge0mulc1cn  34238  lmxrge0  34249  esumpfinvallem  34371  esumcocn  34377  hasheuni  34382  esumcvg  34383  rossros  34477  measinblem  34517  aean  34541  sxbrsigalem3  34569  dya2iocival  34570  dya2iocucvr  34581  sxbrsigalem1  34582  sxbrsigalem2  34583  sxbrsigalem5  34585  sxbrsiga  34587  fiunelcarsg  34613  eulerpartlem1  34664  eulerpartgbij  34669  fibp1  34698  coinfliplem  34776  coinflipprob  34777  ballotlemfval  34787  ballotth  34835  circlemethhgt  34937  hgt750lem2  34946  bnj1400  35130  bnj66  35155  bnj882  35221  lfuhgr  35468  derang0  35519  subfacp1lem1  35529  subfacp1lem6  35535  kur14lem7  35562  cvmsss2  35624  cvmliftlem8  35642  cvmliftlem10  35644  satfv1lem  35712  msubfval  35874  quad3  36020  bcprod  36088  bccolsum  36089  faclim  36096  pprodcnveq  36231  dfon4  36241  fobigcup  36248  dfiota3  36271  dfrecs2  36300  dfrdg4  36301  dfint3  36302  rankeq1o  36521  refssfne  36718  ssoninhaus  36808  onint1  36809  ttciun  36874  bj-dfnul2  37013  bj-rababw  37366  bj-inrab3  37414  bj-imdiridlem  37677  dissneq  37835  dffinxpf  37879  finxpreclem4  37888  rabiun  38092  ptrest  38118  poimirlem3  38122  poimirlem4  38123  poimirlem13  38132  poimirlem16  38135  poimirlem22  38141  poimirlem26  38145  poimirlem27  38146  poimirlem30  38149  cnambfre  38167  ftc1anclem8  38199  fnopabco  38222  abrexdom  38229  cncfres  38264  scottexf  38667  scott0f  38668  inres2  38746  eqrabi  38755  xpv  38761  dfres4  38798  dmxrn  38886  xrnres  38924  xrnres2  38925  rnqmap  38953  dfsucmap2  38963  dfcoss2  39002  dfcoss4  39004  1cossres  39018  dmcoss2  39043  1cosscnvxrn  39064  dfeqvrels2  39171  dfcoeleqvrels  39204  redundss3  39211  dffunsALTV5  39271  dfpeters2  39473  cdleme3d  40855  cdleme7a  40867  cdleme31sdnN  41011  cdlemk45  41571  420gcd8e4  42623  lcmeprodgcdi  42624  60lcm7e420  42627  420lcm8e840  42628  3lexlogpow5ineq1  42671  3lexlogpow2ineq1  42675  3lexlogpow2ineq2  42676  3lexlogpow5ineq5  42677  aks4d1p1  42693  posbezout  42717  aks6d1c1p4  42728  aks6d1c3  42740  2ap1caineq  42762  sticksstones7  42769  sticksstones12a  42774  sticksstones12  42775  aks6d1c6lem4  42790  imaopab  42850  fmpocos  42852  dfqs3  42855  decaddcom  42893  sumcubes  42922  redvmptabs  42969  readvrec  42971  readvcot  42973  sn-00idlem2  43008  reixi  43032  sum9cubes  43254  mapfzcons  43297  eldioph4b  43388  diophren  43390  pwssplit4  43666  pwfi2f1o  43673  frlmpwfi  43675  mendplusgfval  43758  mendmulrfval  43760  mendvscafval  43763  idomodle  43768  cytpval  43779  arearect  43792  onov0suclim  43851  omabs2  43909  tr3dom  44104  har2o  44122  alephiso2  44134  alephiso3  44135  relintab  44159  dfid7  44188  cnvrcl0  44201  dfrtrcl5  44205  dfrcl3  44251  dfrcl4  44252  comptiunov2i  44282  corcltrcl  44315  neicvgnvo  44691  inductionexd  44731  mnuprdlem2  44849  nznngen  44892  hashnzfz2  44897  lhe4.4ex1a  44905  dvradcnv2  44923  binomcxplemrat  44926  binomcxplemnotnn0  44932  nregmodelf1o  45591  refsum2cnlem1  45617  fiiuncl  45645  iccdifprioo  46092  lptre2pt  46214  limclner  46225  stoweidlem13  46587  stoweidlem32  46606  stoweidlem62  46636  wallispi2lem2  46646  stirlinglem14  46661  dirkertrigeqlem1  46672  dirkercncflem4  46680  fourierdlem42  46723  fourierdlem73  46753  fourierdlem81  46761  fourierdlem92  46772  fourierdlem103  46783  fourierdlem104  46784  fouriercnp  46800  fouriersw  46805  sge0tsms  46954  sge0iunmptlemfi  46987  ovolval5lem3  47228  cnfsmf  47314  nthrucw  47462  lamberte  47482  rnfdmpr  47875  fvmptrabdm  47887  fundcmpsurinjlem1  48004  m11nprm  48210  ppi1sum  48240  opoeALTV  48305  nfermltl8rev  48364  sbgoldbo  48409  evengpop3  48420  clnbgrcl  48443  clnbgrnvtx0  48449  usgrexmpl2edg  48651  usgrexmpl2nb0  48653  usgrexmpl2nb3  48656  gpg5order  48682  gpgprismgr4cycllem6  48722  cznabel  48882  cznrng  48883  mpomptx2  48957  2sphere  49371  itscnhlinecirc02plem3  49406  inlinecirc02p  49409  dftpos5  49495  tposresg  49499  icccldii  49540  dfnrm2  49553  dfnrm3  49554  elxpcbasex1ALT  49870  elxpcbasex2ALT  49872  dfswapf2  49882  swapf1a  49890  swapf1f1o  49896  swapf2f1oa  49898  swapfida  49901  setc1oterm  50112  setc1ohomfval  50114  setc1ocofval  50115  funcsetc1o  50118  dfinito4  50122  setc1onsubc  50223  islmd  50286  iscmd  50287  initocmd  50290  termolmd  50291  amgmlemALT  50424