Theorem eqtr4i 2762

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 2740	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2759	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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  3eqtr2i  2765  3eqtr2ri  2766  3eqtr4i  2769  3eqtr4ri  2770  rabab  3502  cbvralcsf  3938  cbvrabcsf  3941  dfin5  3956  dfdif2  3957  uneqin  4278  notabw  4303  unrab  4305  inrab  4306  inrab2  4307  difrab  4308  dfrab3ss  4312  rabun2  4313  dfnul2  4325  difid  4370  rabxm  4386  elnelun  4389  abf  4402  difdifdir  4491  dfif3  4542  dfif5  4544  rabsnif  4727  tpidm  4762  ssunpr  4835  sstp  4837  opidg  4892  dfint2  4952  iunrab  5055  uniiun  5061  intiin  5062  iunid  5063  0iin  5067  mptv  5264  dfepfr  5661  epfrc  5662  xpundi  5744  xpundir  5745  csbcnv  5883  resiun2  6002  resopab  6034  mptresid  6050  dffr3  6098  dfse2  6099  cnvun  6142  imaundir  6150  imainrect  6180  cnvcnv2  6192  cnvrescnv  6194  cnvcnvres  6204  dmtpop  6217  rnsnopg  6220  resdifdi  6235  rnco2  6252  dmco  6253  co01  6260  unidmrn  6278  dfdm2  6280  predidm  6327  tz6.26OLD  6349  dfmpt3  6684  mptun  6696  funcocnv2  6858  dffv2  6986  fnasrn  7145  fpr  7154  fmptap  7170  rnmptc  7210  rnmptcOLD  7211  riotav  7373  dmoprab  7513  rnoprab2  7516  mpov  7523  mpomptx  7524  abrexex2g  7955  1stval2  7996  2ndval2  7997  fo1st  7999  fo2nd  8000  xp2  8016  dfoprab4f  8046  offval22  8079  fmpoco  8086  fimaproj  8126  tposmpo  8254  tposconst  8255  recsfval  8387  rdgsucmpt2  8436  frsucmpt2  8446  df2o3  8480  o1p1e2  8546  o2p2e4  8547  oarec  8568  omopthlem2  8665  ecqs  8781  qliftf  8805  erovlem  8813  fset0  8854  mapsnf1o3  8895  ixp0x  8926  omf1o  9081  xpf1o  9145  mapunen  9152  enp1ilem  9284  pwfiOLD  9353  marypha1lem  9434  marypha2lem4  9439  dfoi  9512  infeq5i  9637  oemapso  9683  cantnflem1  9690  rankelop  9875  leweon  10012  r0weon  10013  kmlem11  10161  dju1dif  10173  ackbij1lem16  10236  cf0  10252  cfsmolem  10271  alephsuc3  10581  fpwwe  10647  canthp1lem1  10653  wuncval2  10748  prlem936  11048  m1p1sr  11093  m1m1sr  11094  dfcnqs  11143  ssxr  11290  mul02lem2  11398  addrid  11401  2p2e4  12354  3p2e5  12370  3p3e6  12371  4p2e6  12372  4p3e7  12373  4p4e8  12374  5p2e7  12375  5p3e8  12376  5p4e9  12377  6p2e8  12378  6p3e9  12379  7p2e9  12380  nnzrab  12597  nn0zrab  12598  dec0u  12705  dec0h  12706  decsuc  12715  decsucc  12725  numma  12728  decma  12735  decmac  12736  decma2c  12737  decadd  12738  decaddc  12739  decmul1c  12749  decmul2c  12750  5p5e10  12755  6p4e10  12756  7p3e10  12759  8p2e10  12764  5t5e25  12787  6t6e36  12792  8t6e48  12803  nn0uz  12871  nnuz  12872  xaddcom  13226  x2times  13285  ioomax  13406  iccmax  13407  ioopos  13408  ioorp  13409  prunioo  13465  fseq1p1m1  13582  fzo13pr  13723  fzo0to2pr  13724  fzo0to3tp  13725  om2uzrdg  13928  fzennn  13940  irec  14172  sq10e99m1  14232  facnn  14242  fac0  14243  faclbnd2  14258  faclbnd4lem1  14260  hashfun  14404  hashbclem  14418  hashf1lem1  14422  hashf1lem1OLD  14423  hashf1lem2  14424  fz1isolem  14429  swrdccatin1  14682  swrdccat3blem  14696  s1co  14791  s2eq2s1eq  14894  s3eqs2s1eq  14896  ofs2  14925  dfid5  14981  dfid6  14982  fsumrev2  15735  fsumparts  15759  fsumiun  15774  isumnn0nn  15795  harmonic  15812  fprod2d  15932  bpoly2  16008  bpoly3  16009  bpoly4  16010  ege2le3  16040  cos1bnd  16137  efieq1re  16149  eirrlem  16154  qnnen  16163  cpnnen  16179  ruclem6  16185  3dvds  16281  pwp1fsum  16341  m1bits  16388  algrp1  16518  phiprmpw  16716  prmreclem4  16859  4sqlem11  16895  4sqlem19  16903  dec5dvds  17004  decsplit1  17022  5prm  17049  7prm  17051  1259lem2  17072  1259lem3  17073  1259lem4  17074  1259lem5  17075  1259prm  17076  2503lem1  17077  2503lem2  17078  2503lem3  17079  2503prm  17080  4001lem1  17081  4001lem2  17082  4001lem3  17083  4001lem4  17084  4001prm  17085  strle1  17098  grpbasex  17243  grpplusgx  17244  quslem  17496  xpsrnbas  17524  acsfn1  17612  acsfn2  17614  comfffval2  17652  dfinito2  17963  dftermo2  17964  xpchomfval  18141  xpccofval  18144  1stfval  18153  2ndfval  18156  oduleg  18253  ismgmid  18596  efmndbas  18794  smndex2dnrinv  18838  grpinvfvi  18910  gaorb  19219  elcntr  19242  cntri  19244  cntrsubgnsg  19255  cntrnsg  19256  setsplusg  19262  oppglemOLD  19263  oppgcntr  19280  gsumwrev  19281  symgressbas  19297  symgplusg  19298  symgvalstruct  19312  symgvalstructOLD  19313  symgga  19323  cayleylem1  19328  psgnunilem2  19411  efgval2  19640  efgredlemc  19661  efgcpbllema  19670  frgpnabllem1  19789  gsumzaddlem  19837  mgplemOLD  20040  opprlem  20237  opprlemOLD  20238  oppr0  20247  opprneg  20249  rmodislmod  20772  rmodislmodOLD  20773  rlmscaf  21065  xrsds  21277  gsumfsum  21301  zringunit  21326  pzriprng1  21358  cnmsgngrp  21442  psgnfix2  21462  relt  21478  ocv0  21540  thlle  21561  thlleOLD  21562  thlleval  21563  dsmmval2  21601  frlmip  21643  mplbas  21860  mplplusg  21877  mplmulr  21878  mplvsca2  21884  ressmplbas2  21893  ltbwe  21910  evlslem4  21948  psr1bas2  22033  ply1bas  22038  ply1assa  22042  psr1plusg  22063  psr1vsca  22064  psr1mulr  22065  ply1plusg  22066  ply1vsca  22067  ply1mulr  22068  ply1mpl0  22097  ply1mpl1  22099  coe1mul  22112  matgsum  22259  smadiadetglem1  22493  indistpsx  22833  iuncld  22869  tgrest  22983  resstopn  23010  leordtval2  23036  xkouni  23423  ptclsg  23439  ptuncnv  23631  ptunhmeo  23632  alexsubALTlem4  23874  tsmsf1o  23969  ucnimalem  24105  ressxms  24354  uniretop  24599  cnfldtopn  24618  xrtgioo  24642  zcld  24649  icccmp  24661  xrge0gsumle  24669  xrge0tsms  24670  metnrmlem3  24697  fsum2cn  24709  cnmpopc  24769  oprpiece1res1  24796  oprpiece1res2  24797  evth  24805  evth2  24806  om1opn  24883  pi1xfrf  24900  pi1xfrcnv  24904  pi1cof  24906  clsocv  25098  cncmet  25170  cnflduss  25204  rrxprds  25237  ehlbase  25263  ismbl  25375  shftmbl  25387  ioorinv  25425  itg1addlem4  25548  itg1addlem4OLD  25549  itg2cnlem1  25611  itg0  25629  itgss3  25664  ditgneg  25706  limcdif  25725  limciun  25743  dvexp  25805  dvef  25832  dvcnvrelem2  25871  ftc1  25897  aannenlem2  26181  dvradcnv  26272  pserdvlem2  26280  reefgim  26302  cospi  26322  sincos6thpi  26365  tanregt0  26388  dflog2  26409  logfac  26449  dvlog  26499  cxpexp  26516  cxpmul2  26537  cxpsqrt  26551  dvsqrt  26590  dvcnsqrt  26592  cxpcn2  26595  isosctrlem2  26665  1cubrlem  26687  1cubr  26688  quart1lem  26701  atancj  26756  atanlogaddlem  26759  atansopn  26778  leibpilem2  26787  log2cnv  26790  log2ublem3  26794  birthdaylem1  26797  birthdaylem2  26798  birthday  26800  dfarea  26806  lgamgulmlem5  26879  lgambdd  26883  ftalem3  26921  basellem2  26928  ppiprm  26997  ppinprm  26998  chtprm  26999  chtnprm  27000  ppi2  27016  ppi3  27017  ppiub  27051  chtub  27059  bclbnd  27127  bposlem8  27138  lgsdilem  27171  lgsdir2lem2  27173  lgsquadlem2  27228  lgsquad2lem2  27232  2lgsoddprmlem3c  27259  rplogsum  27374  mulog2sumlem2  27382  pnt2  27460  bdayfo  27524  bday0s  27675  bday1s  27678  old1  27716  addsasslem2  27835  negsbdaylem  27882  muls01  27926  abssnid  28051  istrkg2ld  28145  axsegconlem9  28617  ax5seglem7  28627  iedgedg  28744  uspgrf1oedg  28867  nbgrcl  29026  nbgrnvtx0  29030  rusgrprc  29281  pthsfval  29412  wlkiswwlks2lem4  29560  wlkiswwlks2lem5  29561  clwwlkvbij  29800  konigsbergumgr  29938  ex-pw  30116  ex-xp  30123  ex-rn  30127  nvvop  30296  nvm  30328  cnims  30380  ip0i  30512  ip1ilem  30513  ipdirilem  30516  ipasslem10  30526  h2hva  30661  h2hsm  30662  h2hvs  30664  axhfvadd-zf  30669  axhvcom-zf  30670  axhvass-zf  30671  axhv0cl-zf  30672  axhvaddid-zf  30673  axhfvmul-zf  30674  axhvmulid-zf  30675  axhvmulass-zf  30676  axhvdistr1-zf  30677  axhvdistr2-zf  30678  axhvmul0-zf  30679  axhfi-zf  30680  axhis1-zf  30681  axhis2-zf  30682  axhis3-zf  30683  axhis4-zf  30684  axhcompl-zf  30685  normlem0  30796  normlem1  30797  normlem2  30798  normlem4  30800  normlem9  30805  bcseqi  30807  dfhnorm2  30809  norm3difi  30834  normpari  30841  normpar2i  30843  polid2i  30844  polidi  30845  hhba  30854  hhims  30859  hhims2  30860  hhsssh  30956  hhssims  30961  hhssims2  30962  shsval3i  31075  dfch2  31094  cmcm2i  31280  fh2  31306  qlaxr3i  31323  spansnji  31333  pjcji  31371  ho0val  31437  df0op2  31439  hosd1i  31509  hosd2i  31510  eigorthi  31524  hhlnoi  31587  hhnmoi  31588  hhbloi  31589  bra0  31637  nmop0  31673  nmfn0  31674  lnopeq0lem1  31692  lnopunilem1  31697  lnophmlem2  31704  nmopcoadji  31788  pjhmopidm  31870  cvmdi  32011  cdj3lem3  32125  cdj3lem3b  32127  abrexdomjm  32178  uniin1  32217  uniin2  32218  iundifdifd  32227  iundifdif  32228  mpomptxf  32339  df1stres  32359  df2ndres  32360  intimafv  32366  fcobijfs  32382  resf1o  32389  fpwrelmapffslem  32391  dpval3  32494  dp3mul10  32498  dpadd2  32510  dpmul4  32514  xrslt  32611  xrsclat  32615  xrge0tsmsd  32646  gsumle  32679  cycpmco2lem7  32728  cycpmconjv  32738  cycpmrn  32739  rndrhmcl  32833  xrge0slmod  32900  lsmsnorb2  32943  qusbas2  32958  rlmdim  33149  rgmoddimOLD  33150  circtopn  33282  tpr2rico  33357  xrge0mulc1cn  33386  lmxrge0  33397  esumpfinvallem  33537  esumcocn  33543  hasheuni  33548  esumcvg  33549  rossros  33643  measinblem  33683  aean  33707  sxbrsigalem3  33736  dya2iocival  33737  dya2iocucvr  33748  sxbrsigalem1  33749  sxbrsigalem2  33750  sxbrsigalem5  33752  sxbrsiga  33754  fiunelcarsg  33780  eulerpartlem1  33831  eulerpartgbij  33836  fibp1  33865  coinfliplem  33942  coinflipprob  33943  ballotlemfval  33953  ballotth  34001  sgnneg  34004  plymulx  34024  circlemethhgt  34120  hgt750lem2  34129  bnj1400  34311  bnj66  34336  bnj882  34402  lfuhgr  34573  derang0  34625  subfacp1lem1  34635  subfacp1lem6  34641  kur14lem7  34668  cvmsss2  34730  cvmliftlem8  34748  cvmliftlem10  34750  satfv1lem  34818  msubfval  34980  quad3  35120  bcprod  35179  bccolsum  35180  faclim  35187  pprodcnveq  35326  dfon4  35336  fobigcup  35343  dfiota3  35366  dfrecs2  35393  dfrdg4  35394  dfint3  35395  rankeq1o  35614  refssfne  35709  ssoninhaus  35799  onint1  35800  bj-rababw  36227  bj-inrab3  36275  bj-imdiridlem  36532  dissneq  36688  dffinxpf  36732  finxpreclem4  36741  rabiun  36927  ptrest  36953  poimirlem3  36957  poimirlem4  36958  poimirlem13  36967  poimirlem16  36970  poimirlem22  36976  poimirlem26  36980  poimirlem27  36981  poimirlem30  36984  cnambfre  37002  ftc1anclem8  37034  fnopabco  37057  abrexdom  37064  cncfres  37099  scottexf  37502  scott0f  37503  inres2  37578  dfres4  37628  xrnres  37738  xrnres2  37739  dfcoss2  37749  dfcoss4  37751  1cossres  37765  dmcoss2  37790  1cosscnvxrn  37811  dfeqvrels2  37924  dfcoeleqvrels  37957  redundss3  37964  dffunsALTV5  38023  cdleme3d  39568  cdleme7a  39580  cdleme31sdnN  39724  cdlemk45  40284  420gcd8e4  41340  lcmeprodgcdi  41341  60lcm7e420  41344  420lcm8e840  41345  3lexlogpow5ineq1  41388  3lexlogpow2ineq1  41392  3lexlogpow2ineq2  41393  3lexlogpow5ineq5  41394  aks4d1p1  41410  2ap1caineq  41430  sticksstones7  41437  sticksstones12a  41442  sticksstones12  41443  imaopab  41519  fmpocos  41525  dfqs2  41528  dfqs3  41529  decaddcom  41661  sumcubes  41676  nn0expgcd  41691  sn-00idlem2  41737  reixi  41760  sum9cubes  41879  mapfzcons  41919  eldioph4b  42014  diophren  42016  pwssplit4  42296  pwfi2f1o  42303  frlmpwfi  42305  mendplusgfval  42392  mendmulrfval  42394  mendvscafval  42397  idomodle  42403  cytpval  42416  arearect  42429  onov0suclim  42489  omabs2  42547  tr3dom  42744  har2o  42762  alephiso2  42774  alephiso3  42775  relintab  42799  dfid7  42828  cnvrcl0  42841  dfrtrcl5  42845  dfrcl3  42891  dfrcl4  42892  comptiunov2i  42922  corcltrcl  42955  neicvgnvo  43331  inductionexd  43371  mnuprdlem2  43497  nznngen  43540  hashnzfz2  43545  lhe4.4ex1a  43553  dvradcnv2  43571  binomcxplemrat  43574  binomcxplemnotnn0  43580  refsum2cnlem1  44186  fiiuncl  44216  iccdifprioo  44690  lptre2pt  44817  limclner  44828  stoweidlem13  45190  stoweidlem32  45209  stoweidlem62  45239  wallispi2lem2  45249  stirlinglem14  45264  dirkertrigeqlem1  45275  dirkercncflem4  45283  fourierdlem42  45326  fourierdlem73  45356  fourierdlem81  45364  fourierdlem92  45375  fourierdlem103  45386  fourierdlem104  45387  fouriercnp  45403  fouriersw  45408  sge0tsms  45557  sge0iunmptlemfi  45590  ovolval5lem3  45831  cnfsmf  45917  rnfdmpr  46450  fvmptrabdm  46462  fundcmpsurinjlem1  46527  m11nprm  46730  opoeALTV  46812  nfermltl8rev  46871  sbgoldbo  46916  evengpop3  46927  cznabel  47099  cznrng  47100  mpomptx2  47175  2sphere  47599  itscnhlinecirc02plem3  47634  inlinecirc02p  47637  icccldii  47715  dfnrm2  47728  dfnrm3  47729  amgmlemALT  48014