Theorem eqtr4i 2768

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  3eqtr2i  2771  3eqtr2ri  2772  3eqtr4i  2775  3eqtr4ri  2776  rabab  3512  cbvralcsf  3941  cbvrabcsf  3944  dfin5  3959  dfdif2  3960  uneqin  4289  notabw  4313  unrab  4315  inrab  4316  inrab2  4317  difrab  4318  dfrab3ss  4323  rabun2  4324  dfnul2  4336  difid  4376  rabxm  4390  elnelun  4393  abf  4406  difdifdir  4492  dfif3  4540  dfif5  4542  rabsnif  4723  tpidm  4758  ssunpr  4834  sstp  4836  opidg  4892  dfint2  4948  iunrab  5052  uniiun  5058  intiin  5059  iunid  5060  0iin  5064  mptv  5258  dfepfr  5669  epfrc  5670  xpundi  5754  xpundir  5755  csbcnv  5894  resiun2  6018  resopab  6052  mptresid  6069  dffr3  6117  dfse2  6118  cnvun  6162  imaundir  6170  imainrect  6201  cnvcnv2  6213  cnvrescnv  6215  cnvcnvres  6225  dmtpop  6238  rnsnopg  6241  resdifdi  6256  rnco2  6273  dmco  6274  co01  6281  unidmrn  6299  dfdm2  6301  predidm  6347  tz6.26OLD  6369  dfmpt3  6702  mptun  6714  funcocnv2  6873  dffv2  7004  fnasrn  7165  fpr  7174  fmptap  7190  rnmptc  7227  riotav  7393  dmoprab  7536  rnoprab2  7539  mpov  7545  mpomptx  7546  abrexex2g  7989  1stval2  8031  2ndval2  8032  fo1st  8034  fo2nd  8035  xp2  8051  dfoprab4f  8081  offval22  8113  fmpoco  8120  fimaproj  8160  tposmpo  8288  tposconst  8289  recsfval  8421  rdgsucmpt2  8470  frsucmpt2  8480  df2o3  8514  o1p1e2  8578  o2p2e4  8579  oarec  8600  omopthlem2  8698  ecqs  8821  qliftf  8845  erovlem  8853  fset0  8894  mapsnf1o3  8935  ixp0x  8966  omf1o  9115  xpf1o  9179  mapunen  9186  enp1ilem  9312  marypha1lem  9473  marypha2lem4  9478  dfoi  9551  infeq5i  9676  oemapso  9722  cantnflem1  9729  rankelop  9914  leweon  10051  r0weon  10052  kmlem11  10201  dju1dif  10213  ackbij1lem16  10274  cf0  10291  cfsmolem  10310  alephsuc3  10620  fpwwe  10686  canthp1lem1  10692  wuncval2  10787  prlem936  11087  m1p1sr  11132  m1m1sr  11133  dfcnqs  11182  ssxr  11330  mul02lem2  11438  addrid  11441  2p2e4  12401  3p2e5  12417  3p3e6  12418  4p2e6  12419  4p3e7  12420  4p4e8  12421  5p2e7  12422  5p3e8  12423  5p4e9  12424  6p2e8  12425  6p3e9  12426  7p2e9  12427  nnzrab  12645  nn0zrab  12646  dec0u  12754  dec0h  12755  decsuc  12764  decsucc  12774  numma  12777  decma  12784  decmac  12785  decma2c  12786  decadd  12787  decaddc  12788  decmul1c  12798  decmul2c  12799  5p5e10  12804  6p4e10  12805  7p3e10  12808  8p2e10  12813  5t5e25  12836  6t6e36  12841  8t6e48  12852  nn0uz  12920  nnuz  12921  xaddcom  13282  x2times  13341  ioomax  13462  iccmax  13463  ioopos  13464  ioorp  13465  prunioo  13521  fseq1p1m1  13638  fzo13pr  13788  fzo0to2pr  13789  fzo0to3tp  13791  om2uzrdg  13997  fzennn  14009  irec  14240  sq10e99m1  14304  facnn  14314  fac0  14315  faclbnd2  14330  faclbnd4lem1  14332  hashfun  14476  hashbclem  14491  hashf1lem1  14494  hashf1lem2  14495  fz1isolem  14500  swrdccatin1  14763  swrdccat3blem  14777  s1co  14872  s2eq2s1eq  14975  s3eqs2s1eq  14977  ofs2  15010  dfid5  15066  dfid6  15067  fsumrev2  15818  fsumparts  15842  fsumiun  15857  isumnn0nn  15878  harmonic  15895  fprod2d  16017  bpoly2  16093  bpoly3  16094  bpoly4  16095  ege2le3  16126  cos1bnd  16223  efieq1re  16235  eirrlem  16240  qnnen  16249  cpnnen  16265  ruclem6  16271  3dvds  16368  pwp1fsum  16428  m1bits  16477  nn0expgcd  16601  algrp1  16611  phiprmpw  16813  prmreclem4  16957  4sqlem11  16993  4sqlem19  17001  dec5dvds  17102  decsplit1  17119  5prm  17146  7prm  17148  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  strle1  17195  grpbasex  17335  grpplusgx  17336  quslem  17588  xpsrnbas  17616  acsfn1  17704  acsfn2  17706  comfffval2  17744  dfinito2  18048  dftermo2  18049  xpchomfval  18224  xpccofval  18227  1stfval  18236  2ndfval  18239  oduleg  18335  ismgmid  18678  efmndbas  18884  smndex2dnrinv  18928  grpinvfvi  19000  gaorb  19325  elcntr  19348  cntri  19350  cntrsubgnsg  19361  cntrnsg  19362  setsplusg  19368  oppglemOLD  19369  oppgcntr  19384  gsumwrev  19385  symgressbas  19399  symgplusg  19400  symgvalstruct  19414  symgvalstructOLD  19415  symgga  19425  cayleylem1  19430  psgnunilem2  19513  efgval2  19742  efgredlemc  19763  efgcpbllema  19772  frgpnabllem1  19891  gsumzaddlem  19939  opprlem  20339  opprlemOLD  20340  oppr0  20349  opprneg  20351  rmodislmod  20928  rlmscaf  21214  xrsds  21427  gsumfsum  21452  zringunit  21477  pzriprng1  21509  cnmsgngrp  21597  psgnfix2  21617  relt  21633  ocv0  21695  thlle  21716  thlleOLD  21717  thlleval  21718  dsmmval2  21756  frlmip  21798  mplbas  22010  mplplusg  22027  mplmulr  22028  mplvsca2  22034  ressmplbas2  22045  ltbwe  22062  evlslem4  22100  psdmul  22170  psr1bas2  22191  ply1bas  22196  ply1basOLD  22197  ply1assa  22201  psr1plusg  22222  psr1vsca  22223  psr1mulr  22224  ply1plusg  22225  ply1vsca  22226  ply1mulr  22227  ply1mpl0  22258  ply1mpl1  22260  coe1mul  22273  matgsum  22443  smadiadetglem1  22677  indistpsx  23017  iuncld  23053  tgrest  23167  resstopn  23194  leordtval2  23220  xkouni  23607  ptclsg  23623  ptuncnv  23815  ptunhmeo  23816  alexsubALTlem4  24058  tsmsf1o  24153  ucnimalem  24289  ressxms  24538  uniretop  24783  cnfldtopn  24802  xrtgioo  24828  zcld  24835  icccmp  24847  xrge0gsumle  24855  xrge0tsms  24856  metnrmlem3  24883  fsum2cn  24895  cnmpopc  24955  oprpiece1res1  24982  oprpiece1res2  24983  evth  24991  evth2  24992  om1opn  25069  pi1xfrf  25086  pi1xfrcnv  25090  pi1cof  25092  clsocv  25284  cncmet  25356  cnflduss  25390  rrxprds  25423  ehlbase  25449  ismbl  25561  shftmbl  25573  ioorinv  25611  itg1addlem4  25734  itg2cnlem1  25796  itg0  25815  itgss3  25850  ditgneg  25892  limcdif  25911  limciun  25929  dvexp  25991  dvef  26018  dvcnvrelem2  26057  ftc1  26083  aannenlem2  26371  dvradcnv  26464  pserdvlem2  26472  reefgim  26494  cospi  26514  sincos6thpi  26558  tanregt0  26581  dflog2  26602  logfac  26643  dvlog  26693  cxpexp  26710  cxpmul2  26731  cxpsqrt  26745  dvsqrt  26784  dvcnsqrt  26786  cxpcn2  26789  isosctrlem2  26862  1cubrlem  26884  1cubr  26885  quart1lem  26898  atancj  26953  atanlogaddlem  26956  atansopn  26975  leibpilem2  26984  log2cnv  26987  log2ublem3  26991  birthdaylem1  26994  birthdaylem2  26995  birthday  26997  dfarea  27003  lgamgulmlem5  27076  lgambdd  27080  ftalem3  27118  basellem2  27125  ppiprm  27194  ppinprm  27195  chtprm  27196  chtnprm  27197  ppi2  27213  ppi3  27214  ppiub  27248  chtub  27256  bclbnd  27324  bposlem8  27335  lgsdilem  27368  lgsdir2lem2  27370  lgsquadlem2  27425  lgsquad2lem2  27429  2lgsoddprmlem3c  27456  rplogsum  27571  mulog2sumlem2  27579  pnt2  27657  bdayfo  27722  bday0s  27873  bday1s  27876  old1  27914  addsasslem2  28037  negsbdaylem  28088  muls01  28138  abssnid  28267  1p1e2s  28400  n0seo  28405  nohalf  28407  zs12bday  28424  istrkg2ld  28468  axsegconlem9  28940  ax5seglem7  28950  iedgedg  29067  uspgrf1oedg  29190  nbgrcl  29352  nbgrnvtx0  29356  rusgrprc  29608  pthsfval  29739  wlkiswwlks2lem4  29892  wlkiswwlks2lem5  29893  clwwlkvbij  30132  konigsbergumgr  30270  ex-pw  30448  ex-xp  30455  ex-rn  30459  nvvop  30628  nvm  30660  cnims  30712  ip0i  30844  ip1ilem  30845  ipdirilem  30848  ipasslem10  30858  h2hva  30993  h2hsm  30994  h2hvs  30996  axhfvadd-zf  31001  axhvcom-zf  31002  axhvass-zf  31003  axhv0cl-zf  31004  axhvaddid-zf  31005  axhfvmul-zf  31006  axhvmulid-zf  31007  axhvmulass-zf  31008  axhvdistr1-zf  31009  axhvdistr2-zf  31010  axhvmul0-zf  31011  axhfi-zf  31012  axhis1-zf  31013  axhis2-zf  31014  axhis3-zf  31015  axhis4-zf  31016  axhcompl-zf  31017  normlem0  31128  normlem1  31129  normlem2  31130  normlem4  31132  normlem9  31137  bcseqi  31139  dfhnorm2  31141  norm3difi  31166  normpari  31173  normpar2i  31175  polid2i  31176  polidi  31177  hhba  31186  hhims  31191  hhims2  31192  hhsssh  31288  hhssims  31293  hhssims2  31294  shsval3i  31407  dfch2  31426  cmcm2i  31612  fh2  31638  qlaxr3i  31655  spansnji  31665  pjcji  31703  ho0val  31769  df0op2  31771  hosd1i  31841  hosd2i  31842  eigorthi  31856  hhlnoi  31919  hhnmoi  31920  hhbloi  31921  bra0  31969  nmop0  32005  nmfn0  32006  lnopeq0lem1  32024  lnopunilem1  32029  lnophmlem2  32036  nmopcoadji  32120  pjhmopidm  32202  cvmdi  32343  cdj3lem3  32457  cdj3lem3b  32459  abrexdomjm  32526  uniin1  32564  uniin2  32565  iundifdifd  32574  iundifdif  32575  mpomptxf  32687  df1stres  32713  df2ndres  32714  intimafv  32720  fcobijfs  32734  resf1o  32741  fpwrelmapffslem  32743  dpval3  32876  dp3mul10  32880  dpadd2  32892  dpmul4  32896  ccatws1f1o  32936  chnub  33002  xrslt  33009  xrsclat  33013  xrge0tsmsd  33065  gsumle  33101  cycpmco2lem7  33152  cycpmconjv  33162  cycpmrn  33163  elrgspnsubrunlem2  33252  rndrhmcl  33299  fracf1  33309  xrge0slmod  33376  lsmsnorb2  33420  qusbas2  33434  1arithidomlem2  33564  zringfrac  33582  rlmdim  33660  rgmoddimOLD  33661  isconstr  33777  circtopn  33836  tpr2rico  33911  xrge0mulc1cn  33940  lmxrge0  33951  esumpfinvallem  34075  esumcocn  34081  hasheuni  34086  esumcvg  34087  rossros  34181  measinblem  34221  aean  34245  sxbrsigalem3  34274  dya2iocival  34275  dya2iocucvr  34286  sxbrsigalem1  34287  sxbrsigalem2  34288  sxbrsigalem5  34290  sxbrsiga  34292  fiunelcarsg  34318  eulerpartlem1  34369  eulerpartgbij  34374  fibp1  34403  coinfliplem  34481  coinflipprob  34482  ballotlemfval  34492  ballotth  34540  sgnneg  34543  plymulx  34563  circlemethhgt  34658  hgt750lem2  34667  bnj1400  34849  bnj66  34874  bnj882  34940  lfuhgr  35123  derang0  35174  subfacp1lem1  35184  subfacp1lem6  35190  kur14lem7  35217  cvmsss2  35279  cvmliftlem8  35297  cvmliftlem10  35299  satfv1lem  35367  msubfval  35529  quad3  35675  bcprod  35738  bccolsum  35739  faclim  35746  pprodcnveq  35884  dfon4  35894  fobigcup  35901  dfiota3  35924  dfrecs2  35951  dfrdg4  35952  dfint3  35953  rankeq1o  36172  refssfne  36359  ssoninhaus  36449  onint1  36450  bj-rababw  36882  bj-inrab3  36930  bj-imdiridlem  37186  dissneq  37342  dffinxpf  37386  finxpreclem4  37395  rabiun  37600  ptrest  37626  poimirlem3  37630  poimirlem4  37631  poimirlem13  37640  poimirlem16  37643  poimirlem22  37649  poimirlem26  37653  poimirlem27  37654  poimirlem30  37657  cnambfre  37675  ftc1anclem8  37707  fnopabco  37730  abrexdom  37737  cncfres  37772  scottexf  38175  scott0f  38176  inres2  38247  dfres4  38294  xrnres  38403  xrnres2  38404  dfcoss2  38414  dfcoss4  38416  1cossres  38430  dmcoss2  38455  1cosscnvxrn  38476  dfeqvrels2  38589  dfcoeleqvrels  38622  redundss3  38629  dffunsALTV5  38688  cdleme3d  40233  cdleme7a  40245  cdleme31sdnN  40389  cdlemk45  40949  420gcd8e4  42007  lcmeprodgcdi  42008  60lcm7e420  42011  420lcm8e840  42012  3lexlogpow5ineq1  42055  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1  42077  posbezout  42101  aks6d1c1p4  42112  aks6d1c3  42124  2ap1caineq  42146  sticksstones7  42153  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem4  42174  imaopab  42270  fmpocos  42275  dfqs2  42278  dfqs3  42279  decaddcom  42319  sumcubes  42347  redvmptabs  42390  readvrec  42392  readvcot  42394  sn-00idlem2  42429  reixi  42452  sum9cubes  42682  mapfzcons  42727  eldioph4b  42822  diophren  42824  pwssplit4  43101  pwfi2f1o  43108  frlmpwfi  43110  mendplusgfval  43193  mendmulrfval  43195  mendvscafval  43198  idomodle  43203  cytpval  43214  arearect  43227  onov0suclim  43287  omabs2  43345  tr3dom  43541  har2o  43559  alephiso2  43571  alephiso3  43572  relintab  43596  dfid7  43625  cnvrcl0  43638  dfrtrcl5  43642  dfrcl3  43688  dfrcl4  43689  comptiunov2i  43719  corcltrcl  43752  neicvgnvo  44128  inductionexd  44168  mnuprdlem2  44292  nznngen  44335  hashnzfz2  44340  lhe4.4ex1a  44348  dvradcnv2  44366  binomcxplemrat  44369  binomcxplemnotnn0  44375  refsum2cnlem1  45042  fiiuncl  45070  iccdifprioo  45529  lptre2pt  45655  limclner  45666  stoweidlem13  46028  stoweidlem32  46047  stoweidlem62  46077  wallispi2lem2  46087  stirlinglem14  46102  dirkertrigeqlem1  46113  dirkercncflem4  46121  fourierdlem42  46164  fourierdlem73  46194  fourierdlem81  46202  fourierdlem92  46213  fourierdlem103  46224  fourierdlem104  46225  fouriercnp  46241  fouriersw  46246  sge0tsms  46395  sge0iunmptlemfi  46428  ovolval5lem3  46669  cnfsmf  46755  rnfdmpr  47293  fvmptrabdm  47305  fundcmpsurinjlem1  47385  m11nprm  47588  opoeALTV  47670  nfermltl8rev  47729  sbgoldbo  47774  evengpop3  47785  clnbgrcl  47808  clnbgrnvtx0  47814  usgrexmpl2edg  47988  usgrexmpl2nb0  47990  usgrexmpl2nb3  47993  gpg5order  48014  cznabel  48176  cznrng  48177  mpomptx2  48251  2sphere  48670  itscnhlinecirc02plem3  48705  inlinecirc02p  48708  dftpos5  48774  tposresg  48778  icccldii  48816  dfnrm2  48829  dfnrm3  48830  elxpcbasex1ALT  48955  elxpcbasex2ALT  48957  dfswapf2  48967  swapf1a  48975  swapf1f1o  48981  swapf2f1oa  48983  swapfida  48986  setc1oterm  49134  amgmlemALT  49322