Theorem eqtr4i 2770

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

Syntax hints:   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731

This theorem is referenced by:  3eqtr2i  2773  3eqtr2ri  2774  3eqtr4i  2777  3eqtr4ri  2778  rabab  3451  cbvralcsf  3874  cbvrabcsf  3877  dfin5  3892  dfdif2  3893  uneqin  4210  notabw  4235  unrab  4237  inrab  4238  inrab2  4239  difrab  4240  dfrab3ss  4244  rabun2  4245  dfnul2  4257  difid  4302  rabxm  4318  elnelun  4321  abf  4334  difdifdir  4420  dfif3  4470  dfif5  4472  rabsnif  4656  tpidm  4691  ssunpr  4762  sstp  4764  opidg  4820  dfint2  4878  iunrab  4978  uniiun  4984  intiin  4985  0iin  4989  mptv  5184  dfepfr  5564  epfrc  5565  xpundi  5645  xpundir  5646  csbcnv  5780  resiun2  5900  resopab  5930  mptresid  5946  opabresidOLD  5947  dffr3  5995  dfse2  5996  cnvun  6034  imaundir  6042  imainrect  6072  cnvcnv2  6084  cnvrescnv  6086  cnvcnvres  6096  dmtpop  6109  rnsnopg  6112  resdifdi  6127  rnco2  6145  dmco  6146  co01  6153  unidmrn  6170  dfdm2  6172  predidm  6215  tz6.26OLD  6233  dfmpt3  6548  mptun  6560  funcocnv2  6721  dffv2  6842  fnasrn  6996  fpr  7005  fmptap  7021  rnmptc  7061  rnmptcOLD  7062  riotav  7214  dmoprab  7351  rnoprab2  7354  mpov  7361  mpomptx  7362  abrexex2g  7777  1stval2  7818  2ndval2  7819  fo1st  7821  fo2nd  7822  xp2  7838  dfoprab4f  7866  offval22  7896  fmpoco  7903  fimaproj  7944  tposmpo  8047  tposconst  8048  recsfval  8159  rdgsucmpt2  8208  frsucmpt2w  8217  frsucmpt2  8218  df2o3  8259  o1p1e2  8309  o2p2e4  8310  o2p2e4OLD  8311  oarec  8332  omopthlem2  8427  ecqs  8505  qliftf  8529  erovlem  8537  fset0  8577  mapsnf1o3  8618  ixp0x  8649  omf1o  8792  xpf1o  8852  mapunen  8859  enp1ilem  8956  pwfiOLD  9019  marypha1lem  9097  marypha2lem4  9102  dfoi  9175  infeq5i  9299  oemapso  9345  cantnflem1  9352  dftrpred2  9372  rankelop  9538  leweon  9673  r0weon  9674  kmlem11  9822  dju1dif  9834  ackbij1lem16  9897  cf0  9913  cfsmolem  9932  alephsuc3  10242  fpwwe  10308  canthp1lem1  10314  wuncval2  10409  prlem936  10709  m1p1sr  10754  m1m1sr  10755  dfcnqs  10804  ssxr  10950  mul02lem2  11057  addid1  11060  2p2e4  12013  3p2e5  12029  3p3e6  12030  4p2e6  12031  4p3e7  12032  4p4e8  12033  5p2e7  12034  5p3e8  12035  5p4e9  12036  6p2e8  12037  6p3e9  12038  7p2e9  12039  nnzrab  12253  nn0zrab  12254  dec0u  12362  dec0h  12363  decsuc  12372  decsucc  12382  numma  12385  decma  12392  decmac  12393  decma2c  12394  decadd  12395  decaddc  12396  decmul1c  12406  decmul2c  12407  5p5e10  12412  6p4e10  12413  7p3e10  12416  8p2e10  12421  5t5e25  12444  6t6e36  12449  8t6e48  12460  nn0uz  12524  nnuz  12525  xaddcom  12878  x2times  12937  ioomax  13058  iccmax  13059  ioopos  13060  ioorp  13061  prunioo  13117  fseq1p1m1  13234  fzo13pr  13374  fzo0to2pr  13375  fzo0to3tp  13376  om2uzrdg  13579  fzennn  13591  irec  13821  sq10e99m1  13882  facnn  13892  fac0  13893  faclbnd2  13908  faclbnd4lem1  13910  hashfun  14055  hashbclem  14067  hashf1lem1  14071  hashf1lem1OLD  14072  hashf1lem2  14073  fz1isolem  14078  swrdccatin1  14341  swrdccat3blem  14355  s1co  14449  s2eq2s1eq  14552  s3eqs2s1eq  14554  ofs2  14585  dfid5  14641  dfid6  14642  fsumrev2  15397  fsumparts  15421  fsumiun  15436  isumnn0nn  15457  harmonic  15474  fprod2d  15594  bpoly2  15670  bpoly3  15671  bpoly4  15672  ege2le3  15702  cos1bnd  15799  efieq1re  15811  eirrlem  15816  qnnen  15825  cpnnen  15841  ruclem6  15847  3dvds  15943  pwp1fsum  16003  m1bits  16050  algrp1  16182  phiprmpw  16380  prmreclem4  16523  4sqlem11  16559  4sqlem19  16567  dec5dvds  16668  decsplit1  16686  5prm  16713  7prm  16715  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  strle1  16762  grpbasex  16902  grpplusgx  16903  quslem  17146  xpsrnbas  17174  acsfn1  17262  acsfn2  17264  comfffval2  17302  dfinito2  17609  dftermo2  17610  xpchomfval  17787  xpccofval  17790  1stfval  17799  2ndfval  17802  oduleg  17899  ismgmid  18239  efmndbas  18400  smndex2dnrinv  18444  grpinvfvi  18512  gaorb  18803  cntri  18827  cntrsubgnsg  18837  cntrnsg  18838  setsplusg  18844  oppglemOLD  18845  oppgcntr  18862  gsumwrev  18863  symgressbas  18879  symgplusg  18880  symgvalstruct  18894  symgvalstructOLD  18895  symgga  18905  cayleylem1  18910  psgnunilem2  18993  efgval2  19220  efgredlemc  19241  efgcpbllema  19250  frgpnabllem1  19364  gsumzaddlem  19412  mgplemOLD  19615  opprlem  19757  opprlemOLD  19758  oppr0  19765  opprneg  19767  rmodislmod  20081  rmodislmodOLD  20082  rlmscaf  20367  xrsds  20528  gsumfsum  20552  zringunit  20575  cnmsgngrp  20671  psgnfix2  20691  relt  20707  ocv0  20769  thlle  20789  thlleval  20790  dsmmval2  20828  frlmip  20870  mplbas  21083  mpladd  21098  mplmul  21100  mplvsca2  21103  ressmplbas2  21113  ltbwe  21130  evlslem4  21169  psr1bas2  21246  ply1bas  21251  ply1assa  21255  mplplusg  21276  mplmulr  21277  psr1plusg  21278  psr1vsca  21279  psr1mulr  21280  ply1plusg  21281  ply1vsca  21282  ply1mulr  21283  ply1mpl0  21311  ply1mpl1  21313  coe1mul  21326  matgsum  21469  smadiadetglem1  21703  indistpsx  22043  iuncld  22079  tgrest  22193  resstopn  22220  leordtval2  22246  xkouni  22633  ptclsg  22649  ptuncnv  22841  ptunhmeo  22842  alexsubALTlem4  23084  tsmsf1o  23179  ucnimalem  23315  ressxms  23562  uniretop  23807  cnfldtopn  23826  xrtgioo  23850  zcld  23857  icccmp  23869  xrge0gsumle  23877  xrge0tsms  23878  metnrmlem3  23905  fsum2cn  23915  cnmpopc  23972  oprpiece1res1  23995  oprpiece1res2  23996  evth  24003  evth2  24004  om1opn  24080  pi1xfrf  24097  pi1xfrcnv  24101  pi1cof  24103  clsocv  24294  cncmet  24366  cnflduss  24400  rrxprds  24433  ehlbase  24459  ismbl  24570  shftmbl  24582  ioorinv  24620  itg1addlem4  24743  itg1addlem4OLD  24744  itg2cnlem1  24806  itg0  24824  itgss3  24859  ditgneg  24901  limcdif  24920  limciun  24938  dvexp  24997  dvef  25024  dvcnvrelem2  25062  ftc1  25086  aannenlem2  25369  dvradcnv  25460  pserdvlem2  25467  reefgim  25489  cospi  25509  sincos6thpi  25552  tanregt0  25575  dflog2  25596  logfac  25636  dvlog  25686  cxpexp  25703  cxpmul2  25724  cxpsqrt  25738  dvsqrt  25775  dvcnsqrt  25777  cxpcn2  25779  isosctrlem2  25849  1cubrlem  25871  1cubr  25872  quart1lem  25885  atancj  25940  atanlogaddlem  25943  atansopn  25962  leibpilem2  25971  log2cnv  25974  log2ublem3  25978  birthdaylem1  25981  birthdaylem2  25982  birthday  25984  dfarea  25990  lgamgulmlem5  26062  lgambdd  26066  ftalem3  26104  basellem2  26111  ppiprm  26180  ppinprm  26181  chtprm  26182  chtnprm  26183  ppi2  26199  ppi3  26200  ppiub  26232  chtub  26240  bclbnd  26308  bposlem8  26319  lgsdilem  26352  lgsdir2lem2  26354  lgsquadlem2  26409  lgsquad2lem2  26413  2lgsoddprmlem3c  26440  rplogsum  26555  mulog2sumlem2  26563  pnt2  26641  istrkg2ld  26700  axsegconlem9  27171  ax5seglem7  27181  iedgedg  27298  uspgrf1oedg  27421  nbgrcl  27580  nbgrnvtx0  27584  rusgrprc  27835  wlkiswwlks2lem4  28113  wlkiswwlks2lem5  28114  clwwlkvbij  28353  konigsbergumgr  28491  ex-pw  28669  ex-xp  28676  ex-rn  28680  nvvop  28847  nvm  28879  cnims  28931  ip0i  29063  ip1ilem  29064  ipdirilem  29067  ipasslem10  29077  h2hva  29212  h2hsm  29213  h2hvs  29215  axhfvadd-zf  29220  axhvcom-zf  29221  axhvass-zf  29222  axhv0cl-zf  29223  axhvaddid-zf  29224  axhfvmul-zf  29225  axhvmulid-zf  29226  axhvmulass-zf  29227  axhvdistr1-zf  29228  axhvdistr2-zf  29229  axhvmul0-zf  29230  axhfi-zf  29231  axhis1-zf  29232  axhis2-zf  29233  axhis3-zf  29234  axhis4-zf  29235  axhcompl-zf  29236  normlem0  29347  normlem1  29348  normlem2  29349  normlem4  29351  normlem9  29356  bcseqi  29358  dfhnorm2  29360  norm3difi  29385  normpari  29392  normpar2i  29394  polid2i  29395  polidi  29396  hhba  29405  hhims  29410  hhims2  29411  hhsssh  29507  hhssims  29512  hhssims2  29513  shsval3i  29626  dfch2  29645  cmcm2i  29831  fh2  29857  qlaxr3i  29874  spansnji  29884  pjcji  29922  ho0val  29988  df0op2  29990  hosd1i  30060  hosd2i  30061  eigorthi  30075  hhlnoi  30138  hhnmoi  30139  hhbloi  30140  bra0  30188  nmop0  30224  nmfn0  30225  lnopeq0lem1  30243  lnopunilem1  30248  lnophmlem2  30255  nmopcoadji  30339  pjhmopidm  30421  cvmdi  30562  cdj3lem3  30676  cdj3lem3b  30678  abrexdomjm  30728  uniin1  30767  uniin2  30768  iundifdifd  30777  iundifdif  30778  mpomptxf  30893  df1stres  30913  df2ndres  30914  intimafv  30920  fcobijfs  30935  resf1o  30942  fpwrelmapffslem  30944  dpval3  31045  dp3mul10  31049  dpadd2  31061  dpmul4  31065  xrslt  31162  xrsclat  31166  xrge0tsmsd  31194  gsumle  31227  cycpmco2lem7  31276  cycpmconjv  31286  cycpmrn  31287  xrge0slmod  31425  lsmsnorb2  31457  rgmoddim  31570  circtopn  31664  tpr2rico  31739  xrge0mulc1cn  31768  lmxrge0  31779  esumpfinvallem  31917  esumcocn  31923  hasheuni  31928  esumcvg  31929  rossros  32023  measinblem  32063  aean  32087  sxbrsigalem3  32114  dya2iocival  32115  dya2iocucvr  32126  sxbrsigalem1  32127  sxbrsigalem2  32128  sxbrsigalem5  32130  sxbrsiga  32132  fiunelcarsg  32158  eulerpartlem1  32209  eulerpartgbij  32214  fibp1  32243  coinfliplem  32320  coinflipprob  32321  ballotlemfval  32331  ballotth  32379  sgnneg  32382  plymulx  32402  circlemethhgt  32498  hgt750lem2  32507  bnj1400  32690  bnj66  32715  bnj882  32781  lfuhgr  32954  derang0  33006  subfacp1lem1  33016  subfacp1lem6  33022  kur14lem7  33049  cvmsss2  33111  cvmliftlem8  33129  cvmliftlem10  33131  satfv1lem  33199  msubfval  33361  quad3  33503  bcprod  33585  bccolsum  33586  faclim  33593  bdayfo  33782  bday0s  33924  bday1s  33927  pprodcnveq  34087  dfon4  34097  fobigcup  34104  dfiota3  34127  dfrecs2  34154  dfrdg4  34155  dfint3  34156  rankeq1o  34375  refssfne  34449  ssoninhaus  34539  onint1  34540  bj-rababw  34968  bj-inrab3  35019  bj-imdiridlem  35259  dissneq  35418  dffinxpf  35462  finxpreclem4  35471  rabiun  35656  ptrest  35682  poimirlem3  35686  poimirlem4  35687  poimirlem13  35696  poimirlem16  35699  poimirlem22  35705  poimirlem26  35709  poimirlem27  35710  poimirlem30  35713  cnambfre  35731  ftc1anclem8  35763  fnopabco  35787  abrexdom  35794  cncfres  35829  scottexf  36232  scott0f  36233  inres2  36290  dfres4  36334  xrnres  36434  xrnres2  36435  dfcoss2  36445  dfcoss4  36447  1cossres  36458  dmcoss2  36478  1cosscnvxrn  36499  dfeqvrels2  36607  dfcoeleqvrels  36640  redundss3  36647  dffunsALTV5  36704  cdleme3d  38151  cdleme7a  38163  cdleme31sdnN  38307  cdlemk45  38867  420gcd8e4  39921  lcmeprodgcdi  39922  60lcm7e420  39925  420lcm8e840  39926  3lexlogpow5ineq1  39969  3lexlogpow2ineq1  39973  3lexlogpow2ineq2  39974  3lexlogpow5ineq5  39975  aks4d1p1  39990  2ap1caineq  40001  sticksstones7  40008  sticksstones12a  40013  sticksstones12  40014  imaopab  40105  dfqs2  40110  dfqs3  40111  decaddcom  40205  nn0expgcd  40228  sn-00idlem2  40275  reixi  40297  mapfzcons  40426  eldioph4b  40521  diophren  40523  pwssplit4  40802  pwfi2f1o  40809  frlmpwfi  40811  mendplusgfval  40898  mendmulrfval  40900  mendvscafval  40903  idomodle  40909  cytpval  40922  arearect  40934  tr3dom  41005  alephiso2  41026  alephiso3  41027  relintab  41052  dfid7  41081  cnvrcl0  41094  dfrtrcl5  41098  dfrcl3  41145  dfrcl4  41146  comptiunov2i  41176  corcltrcl  41209  neicvgnvo  41587  inductionexd  41627  mnuprdlem2  41753  nznngen  41796  hashnzfz2  41801  lhe4.4ex1a  41809  dvradcnv2  41827  binomcxplemrat  41830  binomcxplemnotnn0  41836  refsum2cnlem1  42442  fiiuncl  42475  iccdifprioo  42917  lptre2pt  43044  limclner  43055  stoweidlem13  43417  stoweidlem32  43436  stoweidlem62  43466  wallispi2lem2  43476  stirlinglem14  43491  dirkertrigeqlem1  43502  dirkercncflem4  43510  fourierdlem42  43553  fourierdlem73  43583  fourierdlem81  43591  fourierdlem92  43602  fourierdlem103  43613  fourierdlem104  43614  fouriercnp  43630  fouriersw  43635  sge0tsms  43781  sge0iunmptlemfi  43814  ovolval5lem3  44055  cnfsmf  44136  rnfdmpr  44633  fvmptrabdm  44645  fundcmpsurinjlem1  44711  m11nprm  44914  opoeALTV  44996  nfermltl8rev  45055  sbgoldbo  45100  evengpop3  45111  cznabel  45373  cznrng  45374  mpomptx2  45531  2sphere  45956  itscnhlinecirc02plem3  45991  inlinecirc02p  45994  icccldii  46073  dfnrm2  46086  dfnrm3  46087  amgmlemALT  46366