Theorem eqtr4i 2755

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 2738	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2752	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3eqtr2i  2758  3eqtr2ri  2759  3eqtr4i  2762  3eqtr4ri  2763  rabab  3478  cbvralcsf  3904  cbvrabcsf  3907  dfin5  3922  dfdif2  3923  uneqin  4252  notabw  4276  unrab  4278  inrab  4279  inrab2  4280  difrab  4281  dfrab3ss  4286  rabun2  4287  dfnul2  4299  difid  4339  rabxm  4353  elnelun  4356  abf  4369  difdifdir  4455  dfif3  4503  dfif5  4505  rabsnif  4687  tpidm  4722  ssunpr  4798  sstp  4800  opidg  4856  dfint2  4912  iunrab  5016  uniiun  5022  intiin  5023  iunid  5024  0iin  5028  mptv  5213  dfepfr  5622  epfrc  5623  xpundi  5707  xpundir  5708  csbcnv  5847  resiun2  5971  resopab  6005  mptresid  6022  dffr3  6070  dfse2  6071  cnvun  6115  imaundir  6123  imainrect  6154  cnvcnv2  6166  cnvrescnv  6168  cnvcnvres  6178  dmtpop  6191  rnsnopg  6194  resdifdi  6209  rnco2  6226  dmco  6227  co01  6234  unidmrn  6252  dfdm2  6254  predidm  6299  dfmpt3  6652  mptun  6664  funcocnv2  6825  dffv2  6956  fnasrn  7117  fpr  7126  fmptap  7144  rnmptc  7181  riotav  7349  dmoprab  7492  rnoprab2  7495  mpov  7501  mpomptx  7502  abrexex2g  7943  1stval2  7985  2ndval2  7986  fo1st  7988  fo2nd  7989  xp2  8005  dfoprab4f  8035  offval22  8067  fmpoco  8074  fimaproj  8114  tposmpo  8242  tposconst  8243  recsfval  8349  rdgsucmpt2  8398  frsucmpt2  8408  df2o3  8442  o1p1e2  8504  o2p2e4  8505  oarec  8526  omopthlem2  8624  ecqs  8752  qliftf  8778  erovlem  8786  fset0  8827  mapsnf1o3  8868  ixp0x  8899  omf1o  9044  xpf1o  9103  mapunen  9110  enp1ilem  9223  marypha1lem  9384  marypha2lem4  9389  dfoi  9464  infeq5i  9589  oemapso  9635  cantnflem1  9642  rankelop  9827  leweon  9964  r0weon  9965  kmlem11  10114  dju1dif  10126  ackbij1lem16  10187  cf0  10204  cfsmolem  10223  alephsuc3  10533  fpwwe  10599  canthp1lem1  10605  wuncval2  10700  prlem936  11000  m1p1sr  11045  m1m1sr  11046  dfcnqs  11095  ssxr  11243  mul02lem2  11351  addrid  11354  2p2e4  12316  3p2e5  12332  3p3e6  12333  4p2e6  12334  4p3e7  12335  4p4e8  12336  5p2e7  12337  5p3e8  12338  5p4e9  12339  6p2e8  12340  6p3e9  12341  7p2e9  12342  nnzrab  12561  nn0zrab  12562  dec0u  12670  dec0h  12671  decsuc  12680  decsucc  12690  numma  12693  decma  12700  decmac  12701  decma2c  12702  decadd  12703  decaddc  12704  decmul1c  12714  decmul2c  12715  5p5e10  12720  6p4e10  12721  7p3e10  12724  8p2e10  12729  5t5e25  12752  6t6e36  12757  8t6e48  12768  nn0uz  12835  nnuz  12836  xaddcom  13200  x2times  13259  ioomax  13383  iccmax  13384  ioopos  13385  ioorp  13386  prunioo  13442  fseq1p1m1  13559  fzo13pr  13710  fzo0to2pr  13711  fzo0to3tp  13713  om2uzrdg  13921  fzennn  13933  irec  14166  sq10e99m1  14230  facnn  14240  fac0  14241  faclbnd2  14256  faclbnd4lem1  14258  hashfun  14402  hashbclem  14417  hashf1lem1  14420  hashf1lem2  14421  fz1isolem  14426  swrdccatin1  14690  swrdccat3blem  14704  s1co  14799  s2eq2s1eq  14902  s3eqs2s1eq  14904  ofs2  14937  dfid5  14993  dfid6  14994  fsumrev2  15748  fsumparts  15772  fsumiun  15787  isumnn0nn  15808  harmonic  15825  fprod2d  15947  bpoly2  16023  bpoly3  16024  bpoly4  16025  ege2le3  16056  cos1bnd  16155  efieq1re  16167  eirrlem  16172  qnnen  16181  cpnnen  16197  ruclem6  16203  3dvds  16301  pwp1fsum  16361  m1bits  16410  nn0expgcd  16534  algrp1  16544  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  17506  xpsrnbas  17534  acsfn1  17622  acsfn2  17624  comfffval2  17662  dfinito2  17965  dftermo2  17966  xpchomfval  18140  xpccofval  18143  1stfval  18152  2ndfval  18155  oduleg  18251  ismgmid  18592  efmndbas  18798  smndex2dnrinv  18842  grpinvfvi  18914  gaorb  19239  elcntr  19262  cntri  19264  cntrsubgnsg  19275  cntrnsg  19276  setsplusg  19282  oppgcntr  19297  gsumwrev  19298  symgressbas  19312  symgplusg  19313  symgvalstruct  19327  symgga  19337  cayleylem1  19342  psgnunilem2  19425  efgval2  19654  efgredlemc  19675  efgcpbllema  19684  frgpnabllem1  19803  gsumzaddlem  19851  opprlem  20251  oppr0  20258  opprneg  20260  rmodislmod  20836  rlmscaf  21114  xrsds  21326  gsumfsum  21351  zringunit  21376  pzriprng1  21408  cnmsgngrp  21488  psgnfix2  21508  relt  21524  ocv0  21586  thlle  21606  thlleval  21607  dsmmval2  21645  frlmip  21687  mplbas  21899  mplplusg  21916  mplmulr  21917  mplvsca2  21923  ressmplbas2  21934  ltbwe  21951  evlslem4  21983  psdmul  22053  psr1bas2  22074  ply1bas  22079  ply1basOLD  22080  ply1assa  22084  psr1plusg  22105  psr1vsca  22106  psr1mulr  22107  ply1plusg  22108  ply1vsca  22109  ply1mulr  22110  ply1mpl0  22141  ply1mpl1  22143  coe1mul  22156  matgsum  22324  smadiadetglem1  22558  indistpsx  22897  iuncld  22932  tgrest  23046  resstopn  23073  leordtval2  23099  xkouni  23486  ptclsg  23502  ptuncnv  23694  ptunhmeo  23695  alexsubALTlem4  23937  tsmsf1o  24032  ucnimalem  24167  ressxms  24413  uniretop  24650  cnfldtopn  24669  xrtgioo  24695  zcld  24702  icccmp  24714  xrge0gsumle  24722  xrge0tsms  24723  metnrmlem3  24750  fsum2cn  24762  cnmpopc  24822  oprpiece1res1  24849  oprpiece1res2  24850  evth  24858  evth2  24859  om1opn  24936  pi1xfrf  24953  pi1xfrcnv  24957  pi1cof  24959  clsocv  25150  cncmet  25222  cnflduss  25256  rrxprds  25289  ehlbase  25315  ismbl  25427  shftmbl  25439  ioorinv  25477  itg1addlem4  25600  itg2cnlem1  25662  itg0  25681  itgss3  25716  ditgneg  25758  limcdif  25777  limciun  25795  dvexp  25857  dvef  25884  dvcnvrelem2  25923  ftc1  25949  aannenlem2  26237  dvradcnv  26330  pserdvlem2  26338  reefgim  26360  cospi  26381  sincos6thpi  26425  tanregt0  26448  dflog2  26469  logfac  26510  dvlog  26560  cxpexp  26577  cxpmul2  26598  cxpsqrt  26612  dvsqrt  26651  dvcnsqrt  26653  cxpcn2  26656  isosctrlem2  26729  1cubrlem  26751  1cubr  26752  quart1lem  26765  atancj  26820  atanlogaddlem  26823  atansopn  26842  leibpilem2  26851  log2cnv  26854  log2ublem3  26858  birthdaylem1  26861  birthdaylem2  26862  birthday  26864  dfarea  26870  lgamgulmlem5  26943  lgambdd  26947  ftalem3  26985  basellem2  26992  ppiprm  27061  ppinprm  27062  chtprm  27063  chtnprm  27064  ppi2  27080  ppi3  27081  ppiub  27115  chtub  27123  bclbnd  27191  bposlem8  27202  lgsdilem  27235  lgsdir2lem2  27237  lgsquadlem2  27292  lgsquad2lem2  27296  2lgsoddprmlem3c  27323  rplogsum  27438  mulog2sumlem2  27446  pnt2  27524  bdayfo  27589  bday0s  27740  bday1s  27743  old1  27787  addsasslem2  27911  negsbdaylem  27962  muls01  28015  abssnid  28145  1p1e2s  28302  n0seo  28307  twocut  28309  halfcut  28333  pw2cutp1  28336  zs12bday  28343  istrkg2ld  28387  axsegconlem9  28852  ax5seglem7  28862  iedgedg  28977  uspgrf1oedg  29100  nbgrcl  29262  nbgrnvtx0  29266  rusgrprc  29518  pthsfval  29649  wlkiswwlks2lem4  29802  wlkiswwlks2lem5  29803  clwwlkvbij  30042  konigsbergumgr  30180  ex-pw  30358  ex-xp  30365  ex-rn  30369  nvvop  30538  nvm  30570  cnims  30622  ip0i  30754  ip1ilem  30755  ipdirilem  30758  ipasslem10  30768  h2hva  30903  h2hsm  30904  h2hvs  30906  axhfvadd-zf  30911  axhvcom-zf  30912  axhvass-zf  30913  axhv0cl-zf  30914  axhvaddid-zf  30915  axhfvmul-zf  30916  axhvmulid-zf  30917  axhvmulass-zf  30918  axhvdistr1-zf  30919  axhvdistr2-zf  30920  axhvmul0-zf  30921  axhfi-zf  30922  axhis1-zf  30923  axhis2-zf  30924  axhis3-zf  30925  axhis4-zf  30926  axhcompl-zf  30927  normlem0  31038  normlem1  31039  normlem2  31040  normlem4  31042  normlem9  31047  bcseqi  31049  dfhnorm2  31051  norm3difi  31076  normpari  31083  normpar2i  31085  polid2i  31086  polidi  31087  hhba  31096  hhims  31101  hhims2  31102  hhsssh  31198  hhssims  31203  hhssims2  31204  shsval3i  31317  dfch2  31336  cmcm2i  31522  fh2  31548  qlaxr3i  31565  spansnji  31575  pjcji  31613  ho0val  31679  df0op2  31681  hosd1i  31751  hosd2i  31752  eigorthi  31766  hhlnoi  31829  hhnmoi  31830  hhbloi  31831  bra0  31879  nmop0  31915  nmfn0  31916  lnopeq0lem1  31934  lnopunilem1  31939  lnophmlem2  31946  nmopcoadji  32030  pjhmopidm  32112  cvmdi  32253  cdj3lem3  32367  cdj3lem3b  32369  abrexdomjm  32436  uniin1  32480  uniin2  32481  iundifdifd  32490  iundifdif  32491  mpomptxf  32601  df1stres  32627  df2ndres  32628  intimafv  32634  fcobijfs  32646  resf1o  32653  fpwrelmapffslem  32655  sgnneg  32758  dpval3  32814  dp3mul10  32818  dpadd2  32830  dpmul4  32834  ccatws1f1o  32873  chnub  32938  xrslt  32945  xrsclat  32949  xrge0tsmsd  33002  gsumle  33038  cycpmco2lem7  33089  cycpmconjv  33099  cycpmrn  33100  conjga  33127  elrgspnsubrunlem2  33199  rndrhmcl  33246  fracf1  33257  xrge0slmod  33319  lsmsnorb2  33363  qusbas2  33377  1arithidomlem2  33507  zringfrac  33525  rlmdim  33605  rgmoddimOLD  33606  isconstr  33726  iconstr  33756  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  circtopn  33827  tpr2rico  33902  xrge0mulc1cn  33931  lmxrge0  33942  esumpfinvallem  34064  esumcocn  34070  hasheuni  34075  esumcvg  34076  rossros  34170  measinblem  34210  aean  34234  sxbrsigalem3  34263  dya2iocival  34264  dya2iocucvr  34275  sxbrsigalem1  34276  sxbrsigalem2  34277  sxbrsigalem5  34279  sxbrsiga  34281  fiunelcarsg  34307  eulerpartlem1  34358  eulerpartgbij  34363  fibp1  34392  coinfliplem  34470  coinflipprob  34471  ballotlemfval  34481  ballotth  34529  plymulx  34539  circlemethhgt  34634  hgt750lem2  34643  bnj1400  34825  bnj66  34850  bnj882  34916  lfuhgr  35105  derang0  35156  subfacp1lem1  35166  subfacp1lem6  35172  kur14lem7  35199  cvmsss2  35261  cvmliftlem8  35279  cvmliftlem10  35281  satfv1lem  35349  msubfval  35511  quad3  35657  bcprod  35725  bccolsum  35726  faclim  35733  pprodcnveq  35871  dfon4  35881  fobigcup  35888  dfiota3  35911  dfrecs2  35938  dfrdg4  35939  dfint3  35940  rankeq1o  36159  refssfne  36346  ssoninhaus  36436  onint1  36437  bj-rababw  36869  bj-inrab3  36917  bj-imdiridlem  37173  dissneq  37329  dffinxpf  37373  finxpreclem4  37382  rabiun  37587  ptrest  37613  poimirlem3  37617  poimirlem4  37618  poimirlem13  37627  poimirlem16  37630  poimirlem22  37636  poimirlem26  37640  poimirlem27  37641  poimirlem30  37644  cnambfre  37662  ftc1anclem8  37694  fnopabco  37717  abrexdom  37724  cncfres  37759  scottexf  38162  scott0f  38163  inres2  38234  dfres4  38281  dmxrn  38360  xrnres  38388  xrnres2  38389  dfcoss2  38404  dfcoss4  38406  1cossres  38420  dmcoss2  38445  1cosscnvxrn  38466  dfeqvrels2  38579  dfcoeleqvrels  38612  redundss3  38619  dffunsALTV5  38679  cdleme3d  40225  cdleme7a  40237  cdleme31sdnN  40381  cdlemk45  40941  420gcd8e4  41994  lcmeprodgcdi  41995  60lcm7e420  41998  420lcm8e840  41999  3lexlogpow5ineq1  42042  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1  42064  posbezout  42088  aks6d1c1p4  42099  aks6d1c3  42111  2ap1caineq  42133  sticksstones7  42140  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem4  42161  imaopab  42219  fmpocos  42222  dfqs2  42225  dfqs3  42226  decaddcom  42272  sumcubes  42301  redvmptabs  42348  readvrec  42350  readvcot  42352  sn-00idlem2  42387  reixi  42411  sum9cubes  42660  mapfzcons  42704  eldioph4b  42799  diophren  42801  pwssplit4  43078  pwfi2f1o  43085  frlmpwfi  43087  mendplusgfval  43170  mendmulrfval  43172  mendvscafval  43175  idomodle  43180  cytpval  43191  arearect  43204  onov0suclim  43263  omabs2  43321  tr3dom  43517  har2o  43535  alephiso2  43547  alephiso3  43548  relintab  43572  dfid7  43601  cnvrcl0  43614  dfrtrcl5  43618  dfrcl3  43664  dfrcl4  43665  comptiunov2i  43695  corcltrcl  43728  neicvgnvo  44104  inductionexd  44144  mnuprdlem2  44262  nznngen  44305  hashnzfz2  44310  lhe4.4ex1a  44318  dvradcnv2  44336  binomcxplemrat  44339  binomcxplemnotnn0  44345  nregmodelf1o  45005  refsum2cnlem1  45031  fiiuncl  45059  iccdifprioo  45514  lptre2pt  45638  limclner  45649  stoweidlem13  46011  stoweidlem32  46030  stoweidlem62  46060  wallispi2lem2  46070  stirlinglem14  46085  dirkertrigeqlem1  46096  dirkercncflem4  46104  fourierdlem42  46147  fourierdlem73  46177  fourierdlem81  46185  fourierdlem92  46196  fourierdlem103  46207  fourierdlem104  46208  fouriercnp  46224  fouriersw  46229  sge0tsms  46378  sge0iunmptlemfi  46411  ovolval5lem3  46652  cnfsmf  46738  lamberte  46889  rnfdmpr  47282  fvmptrabdm  47294  fundcmpsurinjlem1  47399  m11nprm  47602  opoeALTV  47684  nfermltl8rev  47743  sbgoldbo  47788  evengpop3  47799  clnbgrcl  47822  clnbgrnvtx0  47828  usgrexmpl2edg  48020  usgrexmpl2nb0  48022  usgrexmpl2nb3  48025  gpg5order  48051  gpgprismgr4cycllem6  48090  cznabel  48248  cznrng  48249  mpomptx2  48323  2sphere  48738  itscnhlinecirc02plem3  48773  inlinecirc02p  48776  dftpos5  48862  tposresg  48866  icccldii  48907  dfnrm2  48920  dfnrm3  48921  elxpcbasex1ALT  49238  elxpcbasex2ALT  49240  dfswapf2  49250  swapf1a  49258  swapf1f1o  49264  swapf2f1oa  49266  swapfida  49269  setc1oterm  49480  setc1ohomfval  49482  setc1ocofval  49483  funcsetc1o  49486  dfinito4  49490  setc1onsubc  49591  islmd  49654  iscmd  49655  initocmd  49658  termolmd  49659  amgmlemALT  49792