Theorem eqtr4i 2795

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  3eqtr2i  2798  3eqtr2ri  2799  3eqtr4i  2802  3eqtr4ri  2803  rabab  3493  cbvralcsf  3903  cbvrabcsf  3906  dfin5  3921  dfdif2  3922  uneqin  4250  notabw  4274  unrab  4276  inrab  4277  inrab2  4278  difrab  4279  dfrab3ss  4284  rabun2  4285  dfnul2  4297  difid  4339  rabxm  4354  elnelun  4357  abf  4377  difdifdir  4457  dfif3  4507  dfif5  4509  rabsnif  4694  tpidm  4729  ssunpr  4803  sstp  4805  opidg  4861  dfint2  4918  iunrab  5021  uniiun  5027  intiin  5028  iunid  5029  0iin  5032  uniin1  5043  uniin2  5044  mptv  5221  dfepfr  5646  epfrc  5647  xpundi  5731  xpundir  5732  csbcnv  5873  csbcnvOLD  5874  resiun2  6000  resopab  6037  mptresid  6054  dffr3  6102  dfse2  6103  cnvun  6140  imaundir  6149  imainrect  6180  cnvcnv2  6192  cnvrescnv  6195  cnvcnvres  6207  dmtpop  6220  rnsnopg  6223  resdifdi  6238  rnco2  6256  dmco  6257  co01  6264  unidmrn  6281  dfdm2  6283  predidm  6328  dfmpt3  6670  mptun  6682  funcocnv2  6847  dffv2  6977  fnasrn  7142  fpr  7152  fmptap  7169  rnmptc  7206  riotav  7373  dmoprab  7514  rnoprab2  7517  mpov  7523  mpomptx  7524  abrexex2g  7960  1stval2  8002  2ndval2  8003  fo1st  8005  fo2nd  8006  xp2  8022  dfoprab4f  8052  offval22  8082  fmpoco  8089  fimaproj  8130  tposmpo  8258  tposconst  8259  recsfval  8366  rdgsucmpt2  8416  frsucmpt2  8426  df2o3  8460  o1p1e2  8524  o2p2e4  8525  oarec  8546  omopthlem2  8645  dfqs2  8700  ecqs  8776  qliftf  8802  erovlem  8810  fset0  8850  mapsnf1o3  8892  ixp0x  8923  omf1o  9067  xpf1o  9126  mapunen  9133  enp1ilem  9237  marypha1lem  9392  marypha2lem4  9397  dfoi  9472  infeq5i  9604  oemapso  9650  cantnflem1  9657  rankelop  9845  leweon  9994  r0weon  9995  kmlem11  10143  dju1dif  10155  ackbij1lem16  10216  cf0  10233  cfsmolem  10253  alephsuc3  10564  fpwwe  10630  canthp1lem1  10636  wuncval2  10731  prlem936  11031  m1p1sr  11076  m1m1sr  11077  dfcnqs  11126  ssxr  11278  mul02lem2  11386  addrid  11389  2p2e4  12374  3p2e5  12390  3p3e6  12391  4p2e6  12392  4p3e7  12393  4p4e8  12394  5p2e7  12395  5p3e8  12396  5p4e9  12397  6p2e8  12398  6p3e9  12399  7p2e9  12400  nnzrab  12621  nn0zrab  12622  dec0u  12736  dec0h  12737  decsuc  12746  decsucc  12756  numma  12759  decma  12766  decmac  12767  decma2c  12768  decadd  12769  decaddc  12770  decmul1c  12780  decmul2c  12781  5p5e10  12786  6p4e10  12787  7p3e10  12790  8p2e10  12795  5t5e25  12818  6t6e36  12823  8t6e48  12834  nn0uz  12899  nnuz  12900  xaddcom  13265  x2times  13324  ioomax  13448  iccmax  13449  ioopos  13450  ioorp  13451  prunioo  13507  fseq1p1m1  13625  fzo13pr  13777  fzo0to2pr  13778  fzo0to3tp  13780  om2uzrdg  13991  fzennn  14003  irec  14236  sq10e99m1  14300  facnn  14310  fac0  14311  faclbnd2  14326  faclbnd4lem1  14328  hashfun  14473  hashbclem  14488  hashf1lem1  14491  hashf1lem2  14492  fz1isolem  14497  swrdccatin1  14761  swrdccat3blem  14775  s1co  14869  s2eq2s1eq  14972  s3eqs2s1eq  14974  ofs2  15007  dfid5  15063  dfid6  15064  sgnneg  15136  fsumrev2  15832  fsumparts  15857  fsumiun  15872  isumnn0nn  15895  harmonic  15912  fprod2d  16034  bpoly2  16110  bpoly3  16111  bpoly4  16112  ege2le3  16143  cos1bnd  16242  efieq1re  16254  eirrlem  16259  qnnen  16268  cpnnen  16284  ruclem6  16290  3dvds  16388  pwp1fsum  16448  m1bits  16497  nn0expgcd  16621  algrp1  16631  phiprmpw  16834  prmreclem4  16978  4sqlem11  17014  4sqlem19  17022  dec5dvds  17123  decsplit1  17140  5prm  17167  7prm  17169  1259lem2  17191  1259lem3  17192  1259lem4  17193  1259lem5  17194  1259prm  17195  2503lem1  17196  2503lem2  17197  2503lem3  17198  2503prm  17199  4001lem1  17200  4001lem2  17201  4001lem3  17202  4001lem4  17203  4001prm  17204  strle1  17217  grpbasex  17344  grpplusgx  17345  quslem  17596  xpsrnbas  17624  acsfn1  17716  acsfn2  17718  comfffval2  17756  dfinito2  18059  dftermo2  18060  xpchomfval  18234  xpccofval  18237  1stfval  18246  2ndfval  18249  oduleg  18345  chnub  18677  ismgmid  18722  efmndbas  18929  smndex2dnrinv  18976  grpinvfvi  19048  gaorb  19376  elcntr  19399  cntri  19401  cntrsubgnsg  19412  cntrnsg  19413  setsplusg  19419  oppgcntr  19434  gsumwrev  19435  symgressbas  19451  symgplusg  19452  symgvalstruct  19466  symgga  19476  cayleylem1  19481  psgnunilem2  19564  efgval2  19793  efgredlemc  19814  efgcpbllema  19823  frgpnabllem1  19942  gsumzaddlem  19990  gsumle  20214  opprlem  20423  oppr0  20430  opprneg  20432  rmodislmod  21028  rlmscaf  21305  xrsds  21528  gsumfsum  21552  zringunit  21584  pzriprng1  21616  cnmsgngrp  21697  psgnfix2  21717  relt  21733  ocv0  21795  thlle  21815  thlleval  21816  dsmmval2  21854  frlmip  21896  mplbas  22107  mplplusg  22124  mplmulr  22125  mplvsca2  22131  ressmplbas2  22145  ltbwe  22163  evlslem4  22195  psdmul  22297  psr1bas2  22318  ply1bas  22323  ply1assa  22327  psr1plusg  22348  psr1vsca  22349  psr1mulr  22350  ply1plusg  22351  ply1vsca  22352  ply1mulr  22353  ply1mpl0  22384  ply1mpl1  22386  coe1mul  22399  matgsum  22562  smadiadetglem1  22796  indistpsx  23135  iuncld  23170  tgrest  23284  resstopn  23311  leordtval2  23337  xkouni  23724  ptclsg  23740  ptuncnv  23932  ptunhmeo  23933  alexsubALTlem4  24175  tsmsf1o  24270  ucnimalem  24404  ressxms  24650  uniretop  24887  cnfldtopn  24906  xrtgioo  24932  zcld  24939  icccmp  24951  xrge0gsumle  24959  xrge0tsms  24960  metnrmlem3  24987  fsum2cn  24998  cnmpopc  25055  oprpiece1res1  25078  oprpiece1res2  25079  evth  25086  evth2  25087  om1opn  25163  pi1xfrf  25180  pi1xfrcnv  25184  pi1cof  25186  clsocv  25377  cncmet  25449  cnflduss  25483  rrxprds  25516  ehlbase  25542  ismbl  25653  shftmbl  25665  ioorinv  25703  itg1addlem4  25826  itg2cnlem1  25888  itg0  25907  itgss3  25942  ditgneg  25984  limcdif  26003  limciun  26021  dvexp  26080  dvef  26107  dvcnvrelem2  26145  ftc1  26169  plymulidp  26411  aannenlem2  26458  dvradcnv  26549  pserdvlem2  26556  reefgim  26578  cospi  26602  sincos6thpi  26646  tanregt0  26669  dflog2  26690  logfac  26731  dvlog  26781  cxpexp  26798  cxpmul2  26819  cxpsqrt  26833  dvsqrt  26872  dvcnsqrt  26874  cxpcn2  26876  isosctrlem2  26949  1cubrlem  26971  1cubr  26972  quart1lem  26985  atancj  27040  atanlogaddlem  27043  atansopn  27062  leibpilem2  27071  log2cnv  27074  log2ublem3  27078  birthdaylem1  27081  birthdaylem2  27082  birthday  27084  dfarea  27090  lgamgulmlem5  27162  lgambdd  27166  ftalem3  27204  basellem2  27211  ppiprm  27280  ppinprm  27281  chtprm  27282  chtnprm  27283  ppi2  27299  ppi3  27300  ppiub  27333  chtub  27341  bclbnd  27409  bposlem8  27420  lgsdilem  27453  lgsdir2lem2  27455  lgsquadlem2  27510  lgsquad2lem2  27514  2lgsoddprmlem3c  27541  rplogsum  27656  mulog2sumlem2  27664  pnt2  27742  bdayfo  27806  bday0  27969  bday1  27972  old1  28023  addsasslem2  28162  negbdaylem  28214  muls01  28270  abssnid  28401  1p1e2s  28574  n0seo  28579  twocut  28581  halfcut  28616  pw2cutp1  28619  pw2cut2  28620  istrkg2ld  28694  axsegconlem9  29215  ax5seglem7  29225  iedgedg  29340  uspgrf1oedg  29463  nbgrcl  29625  nbgrnvtx0  29629  rusgrprc  29880  pthsfval  30008  wlkiswwlks2lem4  30161  wlkiswwlks2lem5  30162  clwwlkvbij  30404  konigsbergumgr  30542  ex-pw  30720  ex-xp  30727  ex-rn  30731  nvvop  30901  nvm  30933  cnims  30985  ip0i  31117  ip1ilem  31118  ipdirilem  31121  ipasslem10  31131  h2hva  31266  h2hsm  31267  h2hvs  31269  axhfvadd-zf  31274  axhvcom-zf  31275  axhvass-zf  31276  axhv0cl-zf  31277  axhvaddid-zf  31278  axhfvmul-zf  31279  axhvmulid-zf  31280  axhvmulass-zf  31281  axhvdistr1-zf  31282  axhvdistr2-zf  31283  axhvmul0-zf  31284  axhfi-zf  31285  axhis1-zf  31286  axhis2-zf  31287  axhis3-zf  31288  axhis4-zf  31289  axhcompl-zf  31290  normlem0  31401  normlem1  31402  normlem2  31403  normlem4  31405  normlem9  31410  bcseqi  31412  dfhnorm2  31414  norm3difi  31439  normpari  31446  normpar2i  31448  polid2i  31449  polidi  31450  hhba  31459  hhims  31464  hhims2  31465  hhsssh  31561  hhssims  31566  hhssims2  31567  shsval3i  31680  dfch2  31699  cmcm2i  31885  fh2  31911  qlaxr3i  31928  spansnji  31938  pjcji  31976  ho0val  32042  df0op2  32044  hosd1i  32114  hosd2i  32115  eigorthi  32129  hhlnoi  32192  hhnmoi  32193  hhbloi  32194  bra0  32242  nmop0  32278  nmfn0  32279  lnopeq0lem1  32297  lnopunilem1  32302  lnophmlem2  32309  nmopcoadji  32393  pjhmopidm  32475  cvmdi  32616  cdj3lem3  32730  cdj3lem3b  32732  abrexdomjm  32793  iundifdifd  32846  iundifdif  32847  mpomptxf  32963  df1stres  32989  df2ndres  32990  intimafv  32996  fcobijfs  33006  fcobijfs2  33007  resf1o  33015  fpwrelmapffslem  33017  dpval3  33153  dp3mul10  33157  dpadd2  33169  dpmul4  33173  ccatws1f1o  33211  xrslt  33267  xrsclat  33271  xrge0tsmsd  33333  cycpmco2lem7  33392  cycpmconjv  33402  cycpmrn  33403  conjga  33430  elrgspnsubrunlem2  33508  rndrhmcl  33559  fracf1  33570  xrge0slmod  33610  lsmsnorb2  33648  qusbas2  33658  1arithidomlem2  33770  zringfrac  33788  selvply1rhm0  33860  mplvrpmga  33879  mplvrpmmhm  33880  mplvrpmrhm  33881  psrmonprod  33886  mplmonprod  33888  vieta  33914  rlmdim  33944  isconstr  34070  iconstr  34100  cos9thpiminplylem4  34119  cos9thpiminplylem5  34120  circtopn  34171  tpr2rico  34246  xrge0mulc1cn  34275  lmxrge0  34286  esumpfinvallem  34408  esumcocn  34414  hasheuni  34419  esumcvg  34420  rossros  34514  measinblem  34554  aean  34578  sxbrsigalem3  34606  dya2iocival  34607  dya2iocucvr  34618  sxbrsigalem1  34619  sxbrsigalem2  34620  sxbrsigalem5  34622  sxbrsiga  34624  fiunelcarsg  34650  eulerpartlem1  34701  eulerpartgbij  34706  fibp1  34735  coinfliplem  34813  coinflipprob  34814  ballotlemfval  34824  ballotth  34872  circlemethhgt  34974  hgt750lem2  34983  bnj1400  35167  bnj66  35192  bnj882  35258  lfuhgr  35508  derang0  35559  subfacp1lem1  35569  subfacp1lem6  35575  kur14lem7  35602  cvmsss2  35664  cvmliftlem8  35682  cvmliftlem10  35684  satfv1lem  35752  msubfval  35914  quad3  36060  bcprod  36128  bccolsum  36129  faclim  36136  pprodcnveq  36271  dfon4  36281  fobigcup  36288  dfiota3  36311  dfrecs2  36340  dfrdg4  36341  dfint3  36342  rankeq1o  36561  refssfne  36757  ssoninhaus  36847  onint1  36848  ttciun  36913  bj-dfnul2  37051  bj-rababw  37404  bj-inrab3  37452  bj-imdiridlem  37716  dissneq  37874  dffinxpf  37918  finxpreclem4  37927  rabiun  38131  ptrest  38157  poimirlem3  38161  poimirlem4  38162  poimirlem13  38171  poimirlem16  38174  poimirlem22  38180  poimirlem26  38184  poimirlem27  38185  poimirlem30  38188  cnambfre  38206  ftc1anclem8  38238  fnopabco  38261  abrexdom  38268  cncfres  38303  scottexf  38706  scott0f  38707  inres2  38785  eqrabi  38794  xpv  38800  dfres4  38837  dmxrn  38925  xrnres  38963  xrnres2  38964  rnqmap  38992  dfsucmap2  39002  dfcoss2  39041  dfcoss4  39043  1cossres  39057  dmcoss2  39082  1cosscnvxrn  39103  dfeqvrels2  39210  dfcoeleqvrels  39243  redundss3  39250  dffunsALTV5  39310  dfpeters2  39512  cdleme3d  40894  cdleme7a  40906  cdleme31sdnN  41050  cdlemk45  41610  420gcd8e4  42662  lcmeprodgcdi  42663  60lcm7e420  42666  420lcm8e840  42667  3lexlogpow5ineq1  42710  3lexlogpow2ineq1  42714  3lexlogpow2ineq2  42715  3lexlogpow5ineq5  42716  aks4d1p1  42732  posbezout  42756  aks6d1c1p4  42767  aks6d1c3  42779  2ap1caineq  42801  sticksstones7  42808  sticksstones12a  42813  sticksstones12  42814  aks6d1c6lem4  42829  25or6to4  42862  imaopab  42891  fmpocos  42893  dfqs3  42896  decaddcom  42934  sumcubes  42963  redvmptabs  43010  readvrec  43012  readvcot  43014  sn-00idlem2  43049  reixi  43073  sum9cubes  43295  mapfzcons  43338  eldioph4b  43429  diophren  43431  pwssplit4  43707  pwfi2f1o  43714  frlmpwfi  43716  mendplusgfval  43799  mendmulrfval  43801  mendvscafval  43804  idomodle  43809  cytpval  43820  arearect  43833  onov0suclim  43892  omabs2  43950  tr3dom  44145  har2o  44163  alephiso2  44175  alephiso3  44176  relintab  44200  dfid7  44229  cnvrcl0  44242  dfrtrcl5  44246  dfrcl3  44292  dfrcl4  44293  comptiunov2i  44323  corcltrcl  44356  neicvgnvo  44732  inductionexd  44772  mnuprdlem2  44874  nznngen  44917  hashnzfz2  44922  lhe4.4ex1a  44930  dvradcnv2  44948  binomcxplemrat  44951  binomcxplemnotnn0  44957  nregmodelf1o  45615  refsum2cnlem1  45648  fiiuncl  45676  iccdifprioo  46123  lptre2pt  46245  limclner  46256  stoweidlem13  46618  stoweidlem32  46637  stoweidlem62  46667  wallispi2lem2  46677  stirlinglem14  46692  dirkertrigeqlem1  46703  dirkercncflem4  46711  fourierdlem42  46754  fourierdlem73  46784  fourierdlem81  46792  fourierdlem92  46803  fourierdlem103  46814  fourierdlem104  46815  fouriercnp  46831  fouriersw  46836  sge0tsms  46985  sge0iunmptlemfi  47018  ovolval5lem3  47259  cnfsmf  47345  nthrucw  47493  lamberte  47513  rnfdmpr  47906  fvmptrabdm  47918  fundcmpsurinjlem1  48035  m11nprm  48241  ppi1sum  48271  opoeALTV  48336  nfermltl8rev  48395  sbgoldbo  48440  evengpop3  48451  clnbgrcl  48474  clnbgrnvtx0  48480  usgrexmpl2edg  48682  usgrexmpl2nb0  48684  usgrexmpl2nb3  48687  gpg5order  48713  gpgprismgr4cycllem6  48753  cznabel  48913  cznrng  48914  mpomptx2  48999  2sphere  49413  itscnhlinecirc02plem3  49448  inlinecirc02p  49451  dftpos5  49536  tposresg  49540  icccldii  49581  dfnrm2  49594  dfnrm3  49595  elxpcbasex1ALT  49911  elxpcbasex2ALT  49913  dfswapf2  49923  swapf1a  49931  swapf1f1o  49937  swapf2f1oa  49939  swapfida  49942  setc1oterm  50153  setc1ohomfval  50155  setc1ocofval  50156  funcsetc1o  50159  dfinito4  50163  setc1onsubc  50264  islmd  50327  iscmd  50328  initocmd  50331  termolmd  50332  amgmlemALT  50476