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

Syntax hints:   = wceq 1541

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  3eqtr2i  2765  3eqtr2ri  2766  3eqtr4i  2769  3eqtr4ri  2770  rabab  3471  cbvralcsf  3891  cbvrabcsf  3894  dfin5  3909  dfdif2  3910  uneqin  4241  notabw  4265  unrab  4267  inrab  4268  inrab2  4269  difrab  4270  dfrab3ss  4275  rabun2  4276  dfnul2  4288  difid  4328  rabxm  4342  elnelun  4345  abf  4358  difdifdir  4444  dfif3  4494  dfif5  4496  rabsnif  4680  tpidm  4715  ssunpr  4790  sstp  4792  opidg  4848  dfint2  4904  iunrab  5008  uniiun  5014  intiin  5015  iunid  5016  0iin  5019  mptv  5204  dfepfr  5608  epfrc  5609  xpundi  5693  xpundir  5694  csbcnv  5832  resiun2  5959  resopab  5993  mptresid  6010  dffr3  6058  dfse2  6059  cnvun  6100  imaundir  6108  imainrect  6139  cnvcnv2  6151  cnvrescnv  6153  cnvcnvres  6163  dmtpop  6176  rnsnopg  6179  resdifdi  6194  rnco2  6212  dmco  6213  co01  6220  unidmrn  6237  dfdm2  6239  predidm  6284  dfmpt3  6626  mptun  6638  funcocnv2  6799  dffv2  6929  fnasrn  7090  fpr  7099  fmptap  7116  rnmptc  7153  riotav  7320  dmoprab  7461  rnoprab2  7464  mpov  7470  mpomptx  7471  abrexex2g  7908  1stval2  7950  2ndval2  7951  fo1st  7953  fo2nd  7954  xp2  7970  dfoprab4f  8000  offval22  8030  fmpoco  8037  fimaproj  8077  tposmpo  8205  tposconst  8206  recsfval  8312  rdgsucmpt2  8361  frsucmpt2  8371  df2o3  8405  o1p1e2  8467  o2p2e4  8468  oarec  8489  omopthlem2  8588  ecqs  8716  qliftf  8742  erovlem  8750  fset0  8791  mapsnf1o3  8833  ixp0x  8864  omf1o  9008  xpf1o  9067  mapunen  9074  enp1ilem  9178  marypha1lem  9336  marypha2lem4  9341  dfoi  9416  infeq5i  9545  oemapso  9591  cantnflem1  9598  rankelop  9786  leweon  9921  r0weon  9922  kmlem11  10071  dju1dif  10083  ackbij1lem16  10144  cf0  10161  cfsmolem  10180  alephsuc3  10491  fpwwe  10557  canthp1lem1  10563  wuncval2  10658  prlem936  10958  m1p1sr  11003  m1m1sr  11004  dfcnqs  11053  ssxr  11202  mul02lem2  11310  addrid  11313  2p2e4  12275  3p2e5  12291  3p3e6  12292  4p2e6  12293  4p3e7  12294  4p4e8  12295  5p2e7  12296  5p3e8  12297  5p4e9  12298  6p2e8  12299  6p3e9  12300  7p2e9  12301  nnzrab  12519  nn0zrab  12520  dec0u  12628  dec0h  12629  decsuc  12638  decsucc  12648  numma  12651  decma  12658  decmac  12659  decma2c  12660  decadd  12661  decaddc  12662  decmul1c  12672  decmul2c  12673  5p5e10  12678  6p4e10  12679  7p3e10  12682  8p2e10  12687  5t5e25  12710  6t6e36  12715  8t6e48  12726  nn0uz  12789  nnuz  12790  xaddcom  13155  x2times  13214  ioomax  13338  iccmax  13339  ioopos  13340  ioorp  13341  prunioo  13397  fseq1p1m1  13514  fzo13pr  13665  fzo0to2pr  13666  fzo0to3tp  13668  om2uzrdg  13879  fzennn  13891  irec  14124  sq10e99m1  14188  facnn  14198  fac0  14199  faclbnd2  14214  faclbnd4lem1  14216  hashfun  14360  hashbclem  14375  hashf1lem1  14378  hashf1lem2  14379  fz1isolem  14384  swrdccatin1  14648  swrdccat3blem  14662  s1co  14756  s2eq2s1eq  14859  s3eqs2s1eq  14861  ofs2  14894  dfid5  14950  dfid6  14951  fsumrev2  15705  fsumparts  15729  fsumiun  15744  isumnn0nn  15765  harmonic  15782  fprod2d  15904  bpoly2  15980  bpoly3  15981  bpoly4  15982  ege2le3  16013  cos1bnd  16112  efieq1re  16124  eirrlem  16129  qnnen  16138  cpnnen  16154  ruclem6  16160  3dvds  16258  pwp1fsum  16318  m1bits  16367  nn0expgcd  16491  algrp1  16501  phiprmpw  16703  prmreclem4  16847  4sqlem11  16883  4sqlem19  16891  dec5dvds  16992  decsplit1  17009  5prm  17036  7prm  17038  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  strle1  17085  grpbasex  17212  grpplusgx  17213  quslem  17464  xpsrnbas  17492  acsfn1  17584  acsfn2  17586  comfffval2  17624  dfinito2  17927  dftermo2  17928  xpchomfval  18102  xpccofval  18105  1stfval  18114  2ndfval  18117  oduleg  18213  chnub  18545  ismgmid  18590  efmndbas  18796  smndex2dnrinv  18840  grpinvfvi  18912  gaorb  19236  elcntr  19259  cntri  19261  cntrsubgnsg  19272  cntrnsg  19273  setsplusg  19279  oppgcntr  19294  gsumwrev  19295  symgressbas  19311  symgplusg  19312  symgvalstruct  19326  symgga  19336  cayleylem1  19341  psgnunilem2  19424  efgval2  19653  efgredlemc  19674  efgcpbllema  19683  frgpnabllem1  19802  gsumzaddlem  19850  gsumle  20074  opprlem  20278  oppr0  20285  opprneg  20287  rmodislmod  20881  rlmscaf  21159  xrsds  21364  gsumfsum  21389  zringunit  21421  pzriprng1  21453  cnmsgngrp  21534  psgnfix2  21554  relt  21570  ocv0  21632  thlle  21652  thlleval  21653  dsmmval2  21691  frlmip  21733  mplbas  21945  mplplusg  21962  mplmulr  21963  mplvsca2  21969  ressmplbas2  21982  ltbwe  21999  evlslem4  22031  psdmul  22109  psr1bas2  22130  ply1bas  22135  ply1basOLD  22136  ply1assa  22140  psr1plusg  22161  psr1vsca  22162  psr1mulr  22163  ply1plusg  22164  ply1vsca  22165  ply1mulr  22166  ply1mpl0  22197  ply1mpl1  22199  coe1mul  22212  matgsum  22381  smadiadetglem1  22615  indistpsx  22954  iuncld  22989  tgrest  23103  resstopn  23130  leordtval2  23156  xkouni  23543  ptclsg  23559  ptuncnv  23751  ptunhmeo  23752  alexsubALTlem4  23994  tsmsf1o  24089  ucnimalem  24223  ressxms  24469  uniretop  24706  cnfldtopn  24725  xrtgioo  24751  zcld  24758  icccmp  24770  xrge0gsumle  24778  xrge0tsms  24779  metnrmlem3  24806  fsum2cn  24818  cnmpopc  24878  oprpiece1res1  24905  oprpiece1res2  24906  evth  24914  evth2  24915  om1opn  24992  pi1xfrf  25009  pi1xfrcnv  25013  pi1cof  25015  clsocv  25206  cncmet  25278  cnflduss  25312  rrxprds  25345  ehlbase  25371  ismbl  25483  shftmbl  25495  ioorinv  25533  itg1addlem4  25656  itg2cnlem1  25718  itg0  25737  itgss3  25772  ditgneg  25814  limcdif  25833  limciun  25851  dvexp  25913  dvef  25940  dvcnvrelem2  25979  ftc1  26005  aannenlem2  26293  dvradcnv  26386  pserdvlem2  26394  reefgim  26416  cospi  26437  sincos6thpi  26481  tanregt0  26504  dflog2  26525  logfac  26566  dvlog  26616  cxpexp  26633  cxpmul2  26654  cxpsqrt  26668  dvsqrt  26707  dvcnsqrt  26709  cxpcn2  26712  isosctrlem2  26785  1cubrlem  26807  1cubr  26808  quart1lem  26821  atancj  26876  atanlogaddlem  26879  atansopn  26898  leibpilem2  26907  log2cnv  26910  log2ublem3  26914  birthdaylem1  26917  birthdaylem2  26918  birthday  26920  dfarea  26926  lgamgulmlem5  26999  lgambdd  27003  ftalem3  27041  basellem2  27048  ppiprm  27117  ppinprm  27118  chtprm  27119  chtnprm  27120  ppi2  27136  ppi3  27137  ppiub  27171  chtub  27179  bclbnd  27247  bposlem8  27258  lgsdilem  27291  lgsdir2lem2  27293  lgsquadlem2  27348  lgsquad2lem2  27352  2lgsoddprmlem3c  27379  rplogsum  27494  mulog2sumlem2  27502  pnt2  27580  bdayfo  27645  bday0  27807  bday1  27810  old1  27861  addsasslem2  28000  negbdaylem  28052  muls01  28108  abssnid  28239  1p1e2s  28412  n0seo  28417  twocut  28419  halfcut  28454  pw2cutp1  28457  pw2cut2  28458  istrkg2ld  28532  axsegconlem9  28998  ax5seglem7  29008  iedgedg  29123  uspgrf1oedg  29246  nbgrcl  29408  nbgrnvtx0  29412  rusgrprc  29664  pthsfval  29792  wlkiswwlks2lem4  29945  wlkiswwlks2lem5  29946  clwwlkvbij  30188  konigsbergumgr  30326  ex-pw  30504  ex-xp  30511  ex-rn  30515  nvvop  30684  nvm  30716  cnims  30768  ip0i  30900  ip1ilem  30901  ipdirilem  30904  ipasslem10  30914  h2hva  31049  h2hsm  31050  h2hvs  31052  axhfvadd-zf  31057  axhvcom-zf  31058  axhvass-zf  31059  axhv0cl-zf  31060  axhvaddid-zf  31061  axhfvmul-zf  31062  axhvmulid-zf  31063  axhvmulass-zf  31064  axhvdistr1-zf  31065  axhvdistr2-zf  31066  axhvmul0-zf  31067  axhfi-zf  31068  axhis1-zf  31069  axhis2-zf  31070  axhis3-zf  31071  axhis4-zf  31072  axhcompl-zf  31073  normlem0  31184  normlem1  31185  normlem2  31186  normlem4  31188  normlem9  31193  bcseqi  31195  dfhnorm2  31197  norm3difi  31222  normpari  31229  normpar2i  31231  polid2i  31232  polidi  31233  hhba  31242  hhims  31247  hhims2  31248  hhsssh  31344  hhssims  31349  hhssims2  31350  shsval3i  31463  dfch2  31482  cmcm2i  31668  fh2  31694  qlaxr3i  31711  spansnji  31721  pjcji  31759  ho0val  31825  df0op2  31827  hosd1i  31897  hosd2i  31898  eigorthi  31912  hhlnoi  31975  hhnmoi  31976  hhbloi  31977  bra0  32025  nmop0  32061  nmfn0  32062  lnopeq0lem1  32080  lnopunilem1  32085  lnophmlem2  32092  nmopcoadji  32176  pjhmopidm  32258  cvmdi  32399  cdj3lem3  32513  cdj3lem3b  32515  abrexdomjm  32582  uniin1  32626  uniin2  32627  iundifdifd  32636  iundifdif  32637  mpomptxf  32757  df1stres  32783  df2ndres  32784  intimafv  32790  fcobijfs  32800  fcobijfs2  32801  resf1o  32809  fpwrelmapffslem  32811  sgnneg  32914  dpval3  32975  dp3mul10  32979  dpadd2  32991  dpmul4  32995  ccatws1f1o  33033  xrslt  33089  xrsclat  33093  xrge0tsmsd  33155  cycpmco2lem7  33214  cycpmconjv  33224  cycpmrn  33225  conjga  33252  elrgspnsubrunlem2  33330  rndrhmcl  33378  fracf1  33389  xrge0slmod  33429  lsmsnorb2  33473  qusbas2  33487  1arithidomlem2  33617  zringfrac  33635  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  vieta  33736  rlmdim  33766  rgmoddimOLD  33767  isconstr  33893  iconstr  33923  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  circtopn  33994  tpr2rico  34069  xrge0mulc1cn  34098  lmxrge0  34109  esumpfinvallem  34231  esumcocn  34237  hasheuni  34242  esumcvg  34243  rossros  34337  measinblem  34377  aean  34401  sxbrsigalem3  34429  dya2iocival  34430  dya2iocucvr  34441  sxbrsigalem1  34442  sxbrsigalem2  34443  sxbrsigalem5  34445  sxbrsiga  34447  fiunelcarsg  34473  eulerpartlem1  34524  eulerpartgbij  34529  fibp1  34558  coinfliplem  34636  coinflipprob  34637  ballotlemfval  34647  ballotth  34695  plymulx  34705  circlemethhgt  34800  hgt750lem2  34809  bnj1400  34991  bnj66  35016  bnj882  35082  lfuhgr  35312  derang0  35363  subfacp1lem1  35373  subfacp1lem6  35379  kur14lem7  35406  cvmsss2  35468  cvmliftlem8  35486  cvmliftlem10  35488  satfv1lem  35556  msubfval  35718  quad3  35864  bcprod  35932  bccolsum  35933  faclim  35940  pprodcnveq  36075  dfon4  36085  fobigcup  36092  dfiota3  36115  dfrecs2  36144  dfrdg4  36145  dfint3  36146  rankeq1o  36365  refssfne  36552  ssoninhaus  36642  onint1  36643  bj-rababw  37082  bj-inrab3  37130  bj-imdiridlem  37390  dissneq  37546  dffinxpf  37590  finxpreclem4  37599  rabiun  37794  ptrest  37820  poimirlem3  37824  poimirlem4  37825  poimirlem13  37834  poimirlem16  37837  poimirlem22  37843  poimirlem26  37847  poimirlem27  37848  poimirlem30  37851  cnambfre  37869  ftc1anclem8  37901  fnopabco  37924  abrexdom  37931  cncfres  37966  scottexf  38369  scott0f  38370  inres2  38443  dfres4  38492  dmxrn  38572  xrnres  38610  xrnres2  38611  dfsucmap2  38638  dfcoss2  38676  dfcoss4  38678  1cossres  38692  dmcoss2  38717  1cosscnvxrn  38738  dfeqvrels2  38845  dfcoeleqvrels  38878  redundss3  38885  dffunsALTV5  38946  cdleme3d  40491  cdleme7a  40503  cdleme31sdnN  40647  cdlemk45  41207  420gcd8e4  42260  lcmeprodgcdi  42261  60lcm7e420  42264  420lcm8e840  42265  3lexlogpow5ineq1  42308  3lexlogpow2ineq1  42312  3lexlogpow2ineq2  42313  3lexlogpow5ineq5  42314  aks4d1p1  42330  posbezout  42354  aks6d1c1p4  42365  aks6d1c3  42377  2ap1caineq  42399  sticksstones7  42406  sticksstones12a  42411  sticksstones12  42412  aks6d1c6lem4  42427  imaopab  42487  fmpocos  42490  dfqs2  42493  dfqs3  42494  decaddcom  42539  sumcubes  42568  redvmptabs  42615  readvrec  42617  readvcot  42619  sn-00idlem2  42654  reixi  42678  sum9cubes  42915  mapfzcons  42958  eldioph4b  43053  diophren  43055  pwssplit4  43331  pwfi2f1o  43338  frlmpwfi  43340  mendplusgfval  43423  mendmulrfval  43425  mendvscafval  43428  idomodle  43433  cytpval  43444  arearect  43457  onov0suclim  43516  omabs2  43574  tr3dom  43769  har2o  43787  alephiso2  43799  alephiso3  43800  relintab  43824  dfid7  43853  cnvrcl0  43866  dfrtrcl5  43870  dfrcl3  43916  dfrcl4  43917  comptiunov2i  43947  corcltrcl  43980  neicvgnvo  44356  inductionexd  44396  mnuprdlem2  44514  nznngen  44557  hashnzfz2  44562  lhe4.4ex1a  44570  dvradcnv2  44588  binomcxplemrat  44591  binomcxplemnotnn0  44597  nregmodelf1o  45256  refsum2cnlem1  45282  fiiuncl  45310  iccdifprioo  45762  lptre2pt  45884  limclner  45895  stoweidlem13  46257  stoweidlem32  46276  stoweidlem62  46306  wallispi2lem2  46316  stirlinglem14  46331  dirkertrigeqlem1  46342  dirkercncflem4  46350  fourierdlem42  46393  fourierdlem73  46423  fourierdlem81  46431  fourierdlem92  46442  fourierdlem103  46453  fourierdlem104  46454  fouriercnp  46470  fouriersw  46475  sge0tsms  46624  sge0iunmptlemfi  46657  ovolval5lem3  46898  cnfsmf  46984  nthrucw  47130  lamberte  47134  rnfdmpr  47527  fvmptrabdm  47539  fundcmpsurinjlem1  47644  m11nprm  47847  opoeALTV  47929  nfermltl8rev  47988  sbgoldbo  48033  evengpop3  48044  clnbgrcl  48067  clnbgrnvtx0  48073  usgrexmpl2edg  48275  usgrexmpl2nb0  48277  usgrexmpl2nb3  48280  gpg5order  48306  gpgprismgr4cycllem6  48346  cznabel  48506  cznrng  48507  mpomptx2  48581  2sphere  48995  itscnhlinecirc02plem3  49030  inlinecirc02p  49033  dftpos5  49119  tposresg  49123  icccldii  49164  dfnrm2  49177  dfnrm3  49178  elxpcbasex1ALT  49494  elxpcbasex2ALT  49496  dfswapf2  49506  swapf1a  49514  swapf1f1o  49520  swapf2f1oa  49522  swapfida  49525  setc1oterm  49736  setc1ohomfval  49738  setc1ocofval  49739  funcsetc1o  49742  dfinito4  49746  setc1onsubc  49847  islmd  49910  iscmd  49911  initocmd  49914  termolmd  49915  amgmlemALT  50048