Theorem eqtr4i 2761

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 2744	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2758	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 2707

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

This theorem is referenced by:  3eqtr2i  2764  3eqtr2ri  2765  3eqtr4i  2768  3eqtr4ri  2769  rabab  3491  cbvralcsf  3916  cbvrabcsf  3919  dfin5  3934  dfdif2  3935  uneqin  4264  notabw  4288  unrab  4290  inrab  4291  inrab2  4292  difrab  4293  dfrab3ss  4298  rabun2  4299  dfnul2  4311  difid  4351  rabxm  4365  elnelun  4368  abf  4381  difdifdir  4467  dfif3  4515  dfif5  4517  rabsnif  4699  tpidm  4734  ssunpr  4810  sstp  4812  opidg  4868  dfint2  4924  iunrab  5028  uniiun  5034  intiin  5035  iunid  5036  0iin  5040  mptv  5228  dfepfr  5638  epfrc  5639  xpundi  5723  xpundir  5724  csbcnv  5863  resiun2  5987  resopab  6021  mptresid  6038  dffr3  6086  dfse2  6087  cnvun  6131  imaundir  6139  imainrect  6170  cnvcnv2  6182  cnvrescnv  6184  cnvcnvres  6194  dmtpop  6207  rnsnopg  6210  resdifdi  6225  rnco2  6242  dmco  6243  co01  6250  unidmrn  6268  dfdm2  6270  predidm  6315  tz6.26OLD  6337  dfmpt3  6671  mptun  6683  funcocnv2  6842  dffv2  6973  fnasrn  7134  fpr  7143  fmptap  7161  rnmptc  7198  riotav  7365  dmoprab  7508  rnoprab2  7511  mpov  7517  mpomptx  7518  abrexex2g  7961  1stval2  8003  2ndval2  8004  fo1st  8006  fo2nd  8007  xp2  8023  dfoprab4f  8053  offval22  8085  fmpoco  8092  fimaproj  8132  tposmpo  8260  tposconst  8261  recsfval  8393  rdgsucmpt2  8442  frsucmpt2  8452  df2o3  8486  o1p1e2  8550  o2p2e4  8551  oarec  8572  omopthlem2  8670  ecqs  8793  qliftf  8817  erovlem  8825  fset0  8866  mapsnf1o3  8907  ixp0x  8938  omf1o  9087  xpf1o  9151  mapunen  9158  enp1ilem  9282  marypha1lem  9443  marypha2lem4  9448  dfoi  9523  infeq5i  9648  oemapso  9694  cantnflem1  9701  rankelop  9886  leweon  10023  r0weon  10024  kmlem11  10173  dju1dif  10185  ackbij1lem16  10246  cf0  10263  cfsmolem  10282  alephsuc3  10592  fpwwe  10658  canthp1lem1  10664  wuncval2  10759  prlem936  11059  m1p1sr  11104  m1m1sr  11105  dfcnqs  11154  ssxr  11302  mul02lem2  11410  addrid  11413  2p2e4  12373  3p2e5  12389  3p3e6  12390  4p2e6  12391  4p3e7  12392  4p4e8  12393  5p2e7  12394  5p3e8  12395  5p4e9  12396  6p2e8  12397  6p3e9  12398  7p2e9  12399  nnzrab  12618  nn0zrab  12619  dec0u  12727  dec0h  12728  decsuc  12737  decsucc  12747  numma  12750  decma  12757  decmac  12758  decma2c  12759  decadd  12760  decaddc  12761  decmul1c  12771  decmul2c  12772  5p5e10  12777  6p4e10  12778  7p3e10  12781  8p2e10  12786  5t5e25  12809  6t6e36  12814  8t6e48  12825  nn0uz  12892  nnuz  12893  xaddcom  13254  x2times  13313  ioomax  13437  iccmax  13438  ioopos  13439  ioorp  13440  prunioo  13496  fseq1p1m1  13613  fzo13pr  13763  fzo0to2pr  13764  fzo0to3tp  13766  om2uzrdg  13972  fzennn  13984  irec  14217  sq10e99m1  14281  facnn  14291  fac0  14292  faclbnd2  14307  faclbnd4lem1  14309  hashfun  14453  hashbclem  14468  hashf1lem1  14471  hashf1lem2  14472  fz1isolem  14477  swrdccatin1  14741  swrdccat3blem  14755  s1co  14850  s2eq2s1eq  14953  s3eqs2s1eq  14955  ofs2  14988  dfid5  15044  dfid6  15045  fsumrev2  15796  fsumparts  15820  fsumiun  15835  isumnn0nn  15856  harmonic  15873  fprod2d  15995  bpoly2  16071  bpoly3  16072  bpoly4  16073  ege2le3  16104  cos1bnd  16203  efieq1re  16215  eirrlem  16220  qnnen  16229  cpnnen  16245  ruclem6  16251  3dvds  16348  pwp1fsum  16408  m1bits  16457  nn0expgcd  16581  algrp1  16591  phiprmpw  16793  prmreclem4  16937  4sqlem11  16973  4sqlem19  16981  dec5dvds  17082  decsplit1  17099  5prm  17126  7prm  17128  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  strle1  17175  grpbasex  17304  grpplusgx  17305  quslem  17555  xpsrnbas  17583  acsfn1  17671  acsfn2  17673  comfffval2  17711  dfinito2  18014  dftermo2  18015  xpchomfval  18189  xpccofval  18192  1stfval  18201  2ndfval  18204  oduleg  18300  ismgmid  18641  efmndbas  18847  smndex2dnrinv  18891  grpinvfvi  18963  gaorb  19288  elcntr  19311  cntri  19313  cntrsubgnsg  19324  cntrnsg  19325  setsplusg  19331  oppgcntr  19346  gsumwrev  19347  symgressbas  19361  symgplusg  19362  symgvalstruct  19376  symgga  19386  cayleylem1  19391  psgnunilem2  19474  efgval2  19703  efgredlemc  19724  efgcpbllema  19733  frgpnabllem1  19852  gsumzaddlem  19900  opprlem  20300  oppr0  20307  opprneg  20309  rmodislmod  20885  rlmscaf  21163  xrsds  21375  gsumfsum  21400  zringunit  21425  pzriprng1  21457  cnmsgngrp  21537  psgnfix2  21557  relt  21573  ocv0  21635  thlle  21655  thlleval  21656  dsmmval2  21694  frlmip  21736  mplbas  21948  mplplusg  21965  mplmulr  21966  mplvsca2  21972  ressmplbas2  21983  ltbwe  22000  evlslem4  22032  psdmul  22102  psr1bas2  22123  ply1bas  22128  ply1basOLD  22129  ply1assa  22133  psr1plusg  22154  psr1vsca  22155  psr1mulr  22156  ply1plusg  22157  ply1vsca  22158  ply1mulr  22159  ply1mpl0  22190  ply1mpl1  22192  coe1mul  22205  matgsum  22373  smadiadetglem1  22607  indistpsx  22946  iuncld  22981  tgrest  23095  resstopn  23122  leordtval2  23148  xkouni  23535  ptclsg  23551  ptuncnv  23743  ptunhmeo  23744  alexsubALTlem4  23986  tsmsf1o  24081  ucnimalem  24216  ressxms  24462  uniretop  24699  cnfldtopn  24718  xrtgioo  24744  zcld  24751  icccmp  24763  xrge0gsumle  24771  xrge0tsms  24772  metnrmlem3  24799  fsum2cn  24811  cnmpopc  24871  oprpiece1res1  24898  oprpiece1res2  24899  evth  24907  evth2  24908  om1opn  24985  pi1xfrf  25002  pi1xfrcnv  25006  pi1cof  25008  clsocv  25200  cncmet  25272  cnflduss  25306  rrxprds  25339  ehlbase  25365  ismbl  25477  shftmbl  25489  ioorinv  25527  itg1addlem4  25650  itg2cnlem1  25712  itg0  25731  itgss3  25766  ditgneg  25808  limcdif  25827  limciun  25845  dvexp  25907  dvef  25934  dvcnvrelem2  25973  ftc1  25999  aannenlem2  26287  dvradcnv  26380  pserdvlem2  26388  reefgim  26410  cospi  26431  sincos6thpi  26475  tanregt0  26498  dflog2  26519  logfac  26560  dvlog  26610  cxpexp  26627  cxpmul2  26648  cxpsqrt  26662  dvsqrt  26701  dvcnsqrt  26703  cxpcn2  26706  isosctrlem2  26779  1cubrlem  26801  1cubr  26802  quart1lem  26815  atancj  26870  atanlogaddlem  26873  atansopn  26892  leibpilem2  26901  log2cnv  26904  log2ublem3  26908  birthdaylem1  26911  birthdaylem2  26912  birthday  26914  dfarea  26920  lgamgulmlem5  26993  lgambdd  26997  ftalem3  27035  basellem2  27042  ppiprm  27111  ppinprm  27112  chtprm  27113  chtnprm  27114  ppi2  27130  ppi3  27131  ppiub  27165  chtub  27173  bclbnd  27241  bposlem8  27252  lgsdilem  27285  lgsdir2lem2  27287  lgsquadlem2  27342  lgsquad2lem2  27346  2lgsoddprmlem3c  27373  rplogsum  27488  mulog2sumlem2  27496  pnt2  27574  bdayfo  27639  bday0s  27790  bday1s  27793  old1  27831  addsasslem2  27954  negsbdaylem  28005  muls01  28055  abssnid  28184  1p1e2s  28317  n0seo  28322  nohalf  28324  zs12bday  28341  istrkg2ld  28385  axsegconlem9  28850  ax5seglem7  28860  iedgedg  28975  uspgrf1oedg  29098  nbgrcl  29260  nbgrnvtx0  29264  rusgrprc  29516  pthsfval  29647  wlkiswwlks2lem4  29800  wlkiswwlks2lem5  29801  clwwlkvbij  30040  konigsbergumgr  30178  ex-pw  30356  ex-xp  30363  ex-rn  30367  nvvop  30536  nvm  30568  cnims  30620  ip0i  30752  ip1ilem  30753  ipdirilem  30756  ipasslem10  30766  h2hva  30901  h2hsm  30902  h2hvs  30904  axhfvadd-zf  30909  axhvcom-zf  30910  axhvass-zf  30911  axhv0cl-zf  30912  axhvaddid-zf  30913  axhfvmul-zf  30914  axhvmulid-zf  30915  axhvmulass-zf  30916  axhvdistr1-zf  30917  axhvdistr2-zf  30918  axhvmul0-zf  30919  axhfi-zf  30920  axhis1-zf  30921  axhis2-zf  30922  axhis3-zf  30923  axhis4-zf  30924  axhcompl-zf  30925  normlem0  31036  normlem1  31037  normlem2  31038  normlem4  31040  normlem9  31045  bcseqi  31047  dfhnorm2  31049  norm3difi  31074  normpari  31081  normpar2i  31083  polid2i  31084  polidi  31085  hhba  31094  hhims  31099  hhims2  31100  hhsssh  31196  hhssims  31201  hhssims2  31202  shsval3i  31315  dfch2  31334  cmcm2i  31520  fh2  31546  qlaxr3i  31563  spansnji  31573  pjcji  31611  ho0val  31677  df0op2  31679  hosd1i  31749  hosd2i  31750  eigorthi  31764  hhlnoi  31827  hhnmoi  31828  hhbloi  31829  bra0  31877  nmop0  31913  nmfn0  31914  lnopeq0lem1  31932  lnopunilem1  31937  lnophmlem2  31944  nmopcoadji  32028  pjhmopidm  32110  cvmdi  32251  cdj3lem3  32365  cdj3lem3b  32367  abrexdomjm  32434  uniin1  32478  uniin2  32479  iundifdifd  32488  iundifdif  32489  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  elrgspnsubrunlem2  33189  rndrhmcl  33236  fracf1  33247  xrge0slmod  33309  lsmsnorb2  33353  qusbas2  33367  1arithidomlem2  33497  zringfrac  33515  rlmdim  33595  rgmoddimOLD  33596  isconstr  33716  iconstr  33746  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  circtopn  33814  tpr2rico  33889  xrge0mulc1cn  33918  lmxrge0  33929  esumpfinvallem  34051  esumcocn  34057  hasheuni  34062  esumcvg  34063  rossros  34157  measinblem  34197  aean  34221  sxbrsigalem3  34250  dya2iocival  34251  dya2iocucvr  34262  sxbrsigalem1  34263  sxbrsigalem2  34264  sxbrsigalem5  34266  sxbrsiga  34268  fiunelcarsg  34294  eulerpartlem1  34345  eulerpartgbij  34350  fibp1  34379  coinfliplem  34457  coinflipprob  34458  ballotlemfval  34468  ballotth  34516  plymulx  34526  circlemethhgt  34621  hgt750lem2  34630  bnj1400  34812  bnj66  34837  bnj882  34903  lfuhgr  35086  derang0  35137  subfacp1lem1  35147  subfacp1lem6  35153  kur14lem7  35180  cvmsss2  35242  cvmliftlem8  35260  cvmliftlem10  35262  satfv1lem  35330  msubfval  35492  quad3  35638  bcprod  35701  bccolsum  35702  faclim  35709  pprodcnveq  35847  dfon4  35857  fobigcup  35864  dfiota3  35887  dfrecs2  35914  dfrdg4  35915  dfint3  35916  rankeq1o  36135  refssfne  36322  ssoninhaus  36412  onint1  36413  bj-rababw  36845  bj-inrab3  36893  bj-imdiridlem  37149  dissneq  37305  dffinxpf  37349  finxpreclem4  37358  rabiun  37563  ptrest  37589  poimirlem3  37593  poimirlem4  37594  poimirlem13  37603  poimirlem16  37606  poimirlem22  37612  poimirlem26  37616  poimirlem27  37617  poimirlem30  37620  cnambfre  37638  ftc1anclem8  37670  fnopabco  37693  abrexdom  37700  cncfres  37735  scottexf  38138  scott0f  38139  inres2  38210  dfres4  38257  xrnres  38366  xrnres2  38367  dfcoss2  38377  dfcoss4  38379  1cossres  38393  dmcoss2  38418  1cosscnvxrn  38439  dfeqvrels2  38552  dfcoeleqvrels  38585  redundss3  38592  dffunsALTV5  38651  cdleme3d  40196  cdleme7a  40208  cdleme31sdnN  40352  cdlemk45  40912  420gcd8e4  41965  lcmeprodgcdi  41966  60lcm7e420  41969  420lcm8e840  41970  3lexlogpow5ineq1  42013  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1p1  42035  posbezout  42059  aks6d1c1p4  42070  aks6d1c3  42082  2ap1caineq  42104  sticksstones7  42111  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem4  42132  imaopab  42228  fmpocos  42232  dfqs2  42235  dfqs3  42236  decaddcom  42281  sumcubes  42309  redvmptabs  42350  readvrec  42352  readvcot  42354  sn-00idlem2  42389  reixi  42412  sum9cubes  42642  mapfzcons  42686  eldioph4b  42781  diophren  42783  pwssplit4  43060  pwfi2f1o  43067  frlmpwfi  43069  mendplusgfval  43152  mendmulrfval  43154  mendvscafval  43157  idomodle  43162  cytpval  43173  arearect  43186  onov0suclim  43245  omabs2  43303  tr3dom  43499  har2o  43517  alephiso2  43529  alephiso3  43530  relintab  43554  dfid7  43583  cnvrcl0  43596  dfrtrcl5  43600  dfrcl3  43646  dfrcl4  43647  comptiunov2i  43677  corcltrcl  43710  neicvgnvo  44086  inductionexd  44126  mnuprdlem2  44245  nznngen  44288  hashnzfz2  44293  lhe4.4ex1a  44301  dvradcnv2  44319  binomcxplemrat  44322  binomcxplemnotnn0  44328  refsum2cnlem1  45009  fiiuncl  45037  iccdifprioo  45493  lptre2pt  45617  limclner  45628  stoweidlem13  45990  stoweidlem32  46009  stoweidlem62  46039  wallispi2lem2  46049  stirlinglem14  46064  dirkertrigeqlem1  46075  dirkercncflem4  46083  fourierdlem42  46126  fourierdlem73  46156  fourierdlem81  46164  fourierdlem92  46175  fourierdlem103  46186  fourierdlem104  46187  fouriercnp  46203  fouriersw  46208  sge0tsms  46357  sge0iunmptlemfi  46390  ovolval5lem3  46631  cnfsmf  46717  lamberte  46868  rnfdmpr  47258  fvmptrabdm  47270  fundcmpsurinjlem1  47360  m11nprm  47563  opoeALTV  47645  nfermltl8rev  47704  sbgoldbo  47749  evengpop3  47760  clnbgrcl  47783  clnbgrnvtx0  47789  usgrexmpl2edg  47981  usgrexmpl2nb0  47983  usgrexmpl2nb3  47986  gpg5order  48012  gpgprismgr4cycllem6  48047  cznabel  48183  cznrng  48184  mpomptx2  48258  2sphere  48677  itscnhlinecirc02plem3  48712  inlinecirc02p  48715  dftpos5  48797  tposresg  48801  icccldii  48841  dfnrm2  48854  dfnrm3  48855  elxpcbasex1ALT  49114  elxpcbasex2ALT  49116  dfswapf2  49126  swapf1a  49134  swapf1f1o  49140  swapf2f1oa  49142  swapfida  49145  setc1oterm  49324  setc1ohomfval  49326  setc1ocofval  49327  funcsetc1o  49330  dfinito4  49334  setc1onsubc  49427  islmd  49483  iscmd  49484  amgmlemALT  49615