Theorem eqtr4i 2756

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 2739	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2753	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 2702

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

This theorem is referenced by:  3eqtr2i  2759  3eqtr2ri  2760  3eqtr4i  2763  3eqtr4ri  2764  rabab  3481  cbvralcsf  3907  cbvrabcsf  3910  dfin5  3925  dfdif2  3926  uneqin  4255  notabw  4279  unrab  4281  inrab  4282  inrab2  4283  difrab  4284  dfrab3ss  4289  rabun2  4290  dfnul2  4302  difid  4342  rabxm  4356  elnelun  4359  abf  4372  difdifdir  4458  dfif3  4506  dfif5  4508  rabsnif  4690  tpidm  4725  ssunpr  4801  sstp  4803  opidg  4859  dfint2  4915  iunrab  5019  uniiun  5025  intiin  5026  iunid  5027  0iin  5031  mptv  5216  dfepfr  5625  epfrc  5626  xpundi  5710  xpundir  5711  csbcnv  5850  resiun2  5974  resopab  6008  mptresid  6025  dffr3  6073  dfse2  6074  cnvun  6118  imaundir  6126  imainrect  6157  cnvcnv2  6169  cnvrescnv  6171  cnvcnvres  6181  dmtpop  6194  rnsnopg  6197  resdifdi  6212  rnco2  6229  dmco  6230  co01  6237  unidmrn  6255  dfdm2  6257  predidm  6302  dfmpt3  6655  mptun  6667  funcocnv2  6828  dffv2  6959  fnasrn  7120  fpr  7129  fmptap  7147  rnmptc  7184  riotav  7352  dmoprab  7495  rnoprab2  7498  mpov  7504  mpomptx  7505  abrexex2g  7946  1stval2  7988  2ndval2  7989  fo1st  7991  fo2nd  7992  xp2  8008  dfoprab4f  8038  offval22  8070  fmpoco  8077  fimaproj  8117  tposmpo  8245  tposconst  8246  recsfval  8352  rdgsucmpt2  8401  frsucmpt2  8411  df2o3  8445  o1p1e2  8507  o2p2e4  8508  oarec  8529  omopthlem2  8627  ecqs  8755  qliftf  8781  erovlem  8789  fset0  8830  mapsnf1o3  8871  ixp0x  8902  omf1o  9049  xpf1o  9109  mapunen  9116  enp1ilem  9230  marypha1lem  9391  marypha2lem4  9396  dfoi  9471  infeq5i  9596  oemapso  9642  cantnflem1  9649  rankelop  9834  leweon  9971  r0weon  9972  kmlem11  10121  dju1dif  10133  ackbij1lem16  10194  cf0  10211  cfsmolem  10230  alephsuc3  10540  fpwwe  10606  canthp1lem1  10612  wuncval2  10707  prlem936  11007  m1p1sr  11052  m1m1sr  11053  dfcnqs  11102  ssxr  11250  mul02lem2  11358  addrid  11361  2p2e4  12323  3p2e5  12339  3p3e6  12340  4p2e6  12341  4p3e7  12342  4p4e8  12343  5p2e7  12344  5p3e8  12345  5p4e9  12346  6p2e8  12347  6p3e9  12348  7p2e9  12349  nnzrab  12568  nn0zrab  12569  dec0u  12677  dec0h  12678  decsuc  12687  decsucc  12697  numma  12700  decma  12707  decmac  12708  decma2c  12709  decadd  12710  decaddc  12711  decmul1c  12721  decmul2c  12722  5p5e10  12727  6p4e10  12728  7p3e10  12731  8p2e10  12736  5t5e25  12759  6t6e36  12764  8t6e48  12775  nn0uz  12842  nnuz  12843  xaddcom  13207  x2times  13266  ioomax  13390  iccmax  13391  ioopos  13392  ioorp  13393  prunioo  13449  fseq1p1m1  13566  fzo13pr  13717  fzo0to2pr  13718  fzo0to3tp  13720  om2uzrdg  13928  fzennn  13940  irec  14173  sq10e99m1  14237  facnn  14247  fac0  14248  faclbnd2  14263  faclbnd4lem1  14265  hashfun  14409  hashbclem  14424  hashf1lem1  14427  hashf1lem2  14428  fz1isolem  14433  swrdccatin1  14697  swrdccat3blem  14711  s1co  14806  s2eq2s1eq  14909  s3eqs2s1eq  14911  ofs2  14944  dfid5  15000  dfid6  15001  fsumrev2  15755  fsumparts  15779  fsumiun  15794  isumnn0nn  15815  harmonic  15832  fprod2d  15954  bpoly2  16030  bpoly3  16031  bpoly4  16032  ege2le3  16063  cos1bnd  16162  efieq1re  16174  eirrlem  16179  qnnen  16188  cpnnen  16204  ruclem6  16210  3dvds  16308  pwp1fsum  16368  m1bits  16417  nn0expgcd  16541  algrp1  16551  phiprmpw  16753  prmreclem4  16897  4sqlem11  16933  4sqlem19  16941  dec5dvds  17042  decsplit1  17059  5prm  17086  7prm  17088  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  strle1  17135  grpbasex  17262  grpplusgx  17263  quslem  17513  xpsrnbas  17541  acsfn1  17629  acsfn2  17631  comfffval2  17669  dfinito2  17972  dftermo2  17973  xpchomfval  18147  xpccofval  18150  1stfval  18159  2ndfval  18162  oduleg  18258  ismgmid  18599  efmndbas  18805  smndex2dnrinv  18849  grpinvfvi  18921  gaorb  19246  elcntr  19269  cntri  19271  cntrsubgnsg  19282  cntrnsg  19283  setsplusg  19289  oppgcntr  19304  gsumwrev  19305  symgressbas  19319  symgplusg  19320  symgvalstruct  19334  symgga  19344  cayleylem1  19349  psgnunilem2  19432  efgval2  19661  efgredlemc  19682  efgcpbllema  19691  frgpnabllem1  19810  gsumzaddlem  19858  opprlem  20258  oppr0  20265  opprneg  20267  rmodislmod  20843  rlmscaf  21121  xrsds  21333  gsumfsum  21358  zringunit  21383  pzriprng1  21415  cnmsgngrp  21495  psgnfix2  21515  relt  21531  ocv0  21593  thlle  21613  thlleval  21614  dsmmval2  21652  frlmip  21694  mplbas  21906  mplplusg  21923  mplmulr  21924  mplvsca2  21930  ressmplbas2  21941  ltbwe  21958  evlslem4  21990  psdmul  22060  psr1bas2  22081  ply1bas  22086  ply1basOLD  22087  ply1assa  22091  psr1plusg  22112  psr1vsca  22113  psr1mulr  22114  ply1plusg  22115  ply1vsca  22116  ply1mulr  22117  ply1mpl0  22148  ply1mpl1  22150  coe1mul  22163  matgsum  22331  smadiadetglem1  22565  indistpsx  22904  iuncld  22939  tgrest  23053  resstopn  23080  leordtval2  23106  xkouni  23493  ptclsg  23509  ptuncnv  23701  ptunhmeo  23702  alexsubALTlem4  23944  tsmsf1o  24039  ucnimalem  24174  ressxms  24420  uniretop  24657  cnfldtopn  24676  xrtgioo  24702  zcld  24709  icccmp  24721  xrge0gsumle  24729  xrge0tsms  24730  metnrmlem3  24757  fsum2cn  24769  cnmpopc  24829  oprpiece1res1  24856  oprpiece1res2  24857  evth  24865  evth2  24866  om1opn  24943  pi1xfrf  24960  pi1xfrcnv  24964  pi1cof  24966  clsocv  25157  cncmet  25229  cnflduss  25263  rrxprds  25296  ehlbase  25322  ismbl  25434  shftmbl  25446  ioorinv  25484  itg1addlem4  25607  itg2cnlem1  25669  itg0  25688  itgss3  25723  ditgneg  25765  limcdif  25784  limciun  25802  dvexp  25864  dvef  25891  dvcnvrelem2  25930  ftc1  25956  aannenlem2  26244  dvradcnv  26337  pserdvlem2  26345  reefgim  26367  cospi  26388  sincos6thpi  26432  tanregt0  26455  dflog2  26476  logfac  26517  dvlog  26567  cxpexp  26584  cxpmul2  26605  cxpsqrt  26619  dvsqrt  26658  dvcnsqrt  26660  cxpcn2  26663  isosctrlem2  26736  1cubrlem  26758  1cubr  26759  quart1lem  26772  atancj  26827  atanlogaddlem  26830  atansopn  26849  leibpilem2  26858  log2cnv  26861  log2ublem3  26865  birthdaylem1  26868  birthdaylem2  26869  birthday  26871  dfarea  26877  lgamgulmlem5  26950  lgambdd  26954  ftalem3  26992  basellem2  26999  ppiprm  27068  ppinprm  27069  chtprm  27070  chtnprm  27071  ppi2  27087  ppi3  27088  ppiub  27122  chtub  27130  bclbnd  27198  bposlem8  27209  lgsdilem  27242  lgsdir2lem2  27244  lgsquadlem2  27299  lgsquad2lem2  27303  2lgsoddprmlem3c  27330  rplogsum  27445  mulog2sumlem2  27453  pnt2  27531  bdayfo  27596  bday0s  27747  bday1s  27750  old1  27794  addsasslem2  27918  negsbdaylem  27969  muls01  28022  abssnid  28152  1p1e2s  28309  n0seo  28314  twocut  28316  halfcut  28340  pw2cutp1  28343  zs12bday  28350  istrkg2ld  28394  axsegconlem9  28859  ax5seglem7  28869  iedgedg  28984  uspgrf1oedg  29107  nbgrcl  29269  nbgrnvtx0  29273  rusgrprc  29525  pthsfval  29656  wlkiswwlks2lem4  29809  wlkiswwlks2lem5  29810  clwwlkvbij  30049  konigsbergumgr  30187  ex-pw  30365  ex-xp  30372  ex-rn  30376  nvvop  30545  nvm  30577  cnims  30629  ip0i  30761  ip1ilem  30762  ipdirilem  30765  ipasslem10  30775  h2hva  30910  h2hsm  30911  h2hvs  30913  axhfvadd-zf  30918  axhvcom-zf  30919  axhvass-zf  30920  axhv0cl-zf  30921  axhvaddid-zf  30922  axhfvmul-zf  30923  axhvmulid-zf  30924  axhvmulass-zf  30925  axhvdistr1-zf  30926  axhvdistr2-zf  30927  axhvmul0-zf  30928  axhfi-zf  30929  axhis1-zf  30930  axhis2-zf  30931  axhis3-zf  30932  axhis4-zf  30933  axhcompl-zf  30934  normlem0  31045  normlem1  31046  normlem2  31047  normlem4  31049  normlem9  31054  bcseqi  31056  dfhnorm2  31058  norm3difi  31083  normpari  31090  normpar2i  31092  polid2i  31093  polidi  31094  hhba  31103  hhims  31108  hhims2  31109  hhsssh  31205  hhssims  31210  hhssims2  31211  shsval3i  31324  dfch2  31343  cmcm2i  31529  fh2  31555  qlaxr3i  31572  spansnji  31582  pjcji  31620  ho0val  31686  df0op2  31688  hosd1i  31758  hosd2i  31759  eigorthi  31773  hhlnoi  31836  hhnmoi  31837  hhbloi  31838  bra0  31886  nmop0  31922  nmfn0  31923  lnopeq0lem1  31941  lnopunilem1  31946  lnophmlem2  31953  nmopcoadji  32037  pjhmopidm  32119  cvmdi  32260  cdj3lem3  32374  cdj3lem3b  32376  abrexdomjm  32443  uniin1  32487  uniin2  32488  iundifdifd  32497  iundifdif  32498  mpomptxf  32608  df1stres  32634  df2ndres  32635  intimafv  32641  fcobijfs  32653  resf1o  32660  fpwrelmapffslem  32662  sgnneg  32765  dpval3  32821  dp3mul10  32825  dpadd2  32837  dpmul4  32841  ccatws1f1o  32880  chnub  32945  xrslt  32952  xrsclat  32956  xrge0tsmsd  33009  gsumle  33045  cycpmco2lem7  33096  cycpmconjv  33106  cycpmrn  33107  conjga  33134  elrgspnsubrunlem2  33206  rndrhmcl  33253  fracf1  33264  xrge0slmod  33326  lsmsnorb2  33370  qusbas2  33384  1arithidomlem2  33514  zringfrac  33532  rlmdim  33612  rgmoddimOLD  33613  isconstr  33733  iconstr  33763  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  circtopn  33834  tpr2rico  33909  xrge0mulc1cn  33938  lmxrge0  33949  esumpfinvallem  34071  esumcocn  34077  hasheuni  34082  esumcvg  34083  rossros  34177  measinblem  34217  aean  34241  sxbrsigalem3  34270  dya2iocival  34271  dya2iocucvr  34282  sxbrsigalem1  34283  sxbrsigalem2  34284  sxbrsigalem5  34286  sxbrsiga  34288  fiunelcarsg  34314  eulerpartlem1  34365  eulerpartgbij  34370  fibp1  34399  coinfliplem  34477  coinflipprob  34478  ballotlemfval  34488  ballotth  34536  plymulx  34546  circlemethhgt  34641  hgt750lem2  34650  bnj1400  34832  bnj66  34857  bnj882  34923  lfuhgr  35112  derang0  35163  subfacp1lem1  35173  subfacp1lem6  35179  kur14lem7  35206  cvmsss2  35268  cvmliftlem8  35286  cvmliftlem10  35288  satfv1lem  35356  msubfval  35518  quad3  35664  bcprod  35732  bccolsum  35733  faclim  35740  pprodcnveq  35878  dfon4  35888  fobigcup  35895  dfiota3  35918  dfrecs2  35945  dfrdg4  35946  dfint3  35947  rankeq1o  36166  refssfne  36353  ssoninhaus  36443  onint1  36444  bj-rababw  36876  bj-inrab3  36924  bj-imdiridlem  37180  dissneq  37336  dffinxpf  37380  finxpreclem4  37389  rabiun  37594  ptrest  37620  poimirlem3  37624  poimirlem4  37625  poimirlem13  37634  poimirlem16  37637  poimirlem22  37643  poimirlem26  37647  poimirlem27  37648  poimirlem30  37651  cnambfre  37669  ftc1anclem8  37701  fnopabco  37724  abrexdom  37731  cncfres  37766  scottexf  38169  scott0f  38170  inres2  38241  dfres4  38288  dmxrn  38367  xrnres  38395  xrnres2  38396  dfcoss2  38411  dfcoss4  38413  1cossres  38427  dmcoss2  38452  1cosscnvxrn  38473  dfeqvrels2  38586  dfcoeleqvrels  38619  redundss3  38626  dffunsALTV5  38686  cdleme3d  40232  cdleme7a  40244  cdleme31sdnN  40388  cdlemk45  40948  420gcd8e4  42001  lcmeprodgcdi  42002  60lcm7e420  42005  420lcm8e840  42006  3lexlogpow5ineq1  42049  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1  42071  posbezout  42095  aks6d1c1p4  42106  aks6d1c3  42118  2ap1caineq  42140  sticksstones7  42147  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem4  42168  imaopab  42226  fmpocos  42229  dfqs2  42232  dfqs3  42233  decaddcom  42279  sumcubes  42308  redvmptabs  42355  readvrec  42357  readvcot  42359  sn-00idlem2  42394  reixi  42418  sum9cubes  42667  mapfzcons  42711  eldioph4b  42806  diophren  42808  pwssplit4  43085  pwfi2f1o  43092  frlmpwfi  43094  mendplusgfval  43177  mendmulrfval  43179  mendvscafval  43182  idomodle  43187  cytpval  43198  arearect  43211  onov0suclim  43270  omabs2  43328  tr3dom  43524  har2o  43542  alephiso2  43554  alephiso3  43555  relintab  43579  dfid7  43608  cnvrcl0  43621  dfrtrcl5  43625  dfrcl3  43671  dfrcl4  43672  comptiunov2i  43702  corcltrcl  43735  neicvgnvo  44111  inductionexd  44151  mnuprdlem2  44269  nznngen  44312  hashnzfz2  44317  lhe4.4ex1a  44325  dvradcnv2  44343  binomcxplemrat  44346  binomcxplemnotnn0  44352  nregmodelf1o  45012  refsum2cnlem1  45038  fiiuncl  45066  iccdifprioo  45521  lptre2pt  45645  limclner  45656  stoweidlem13  46018  stoweidlem32  46037  stoweidlem62  46067  wallispi2lem2  46077  stirlinglem14  46092  dirkertrigeqlem1  46103  dirkercncflem4  46111  fourierdlem42  46154  fourierdlem73  46184  fourierdlem81  46192  fourierdlem92  46203  fourierdlem103  46214  fourierdlem104  46215  fouriercnp  46231  fouriersw  46236  sge0tsms  46385  sge0iunmptlemfi  46418  ovolval5lem3  46659  cnfsmf  46745  lamberte  46896  rnfdmpr  47286  fvmptrabdm  47298  fundcmpsurinjlem1  47403  m11nprm  47606  opoeALTV  47688  nfermltl8rev  47747  sbgoldbo  47792  evengpop3  47803  clnbgrcl  47826  clnbgrnvtx0  47832  usgrexmpl2edg  48024  usgrexmpl2nb0  48026  usgrexmpl2nb3  48029  gpg5order  48055  gpgprismgr4cycllem6  48094  cznabel  48252  cznrng  48253  mpomptx2  48327  2sphere  48742  itscnhlinecirc02plem3  48777  inlinecirc02p  48780  dftpos5  48866  tposresg  48870  icccldii  48911  dfnrm2  48924  dfnrm3  48925  elxpcbasex1ALT  49242  elxpcbasex2ALT  49244  dfswapf2  49254  swapf1a  49262  swapf1f1o  49268  swapf2f1oa  49270  swapfida  49273  setc1oterm  49484  setc1ohomfval  49486  setc1ocofval  49487  funcsetc1o  49490  dfinito4  49494  setc1onsubc  49595  islmd  49658  iscmd  49659  initocmd  49662  termolmd  49663  amgmlemALT  49796