Theorem eqtr4i 2764

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  3eqtr2i  2767  3eqtr2ri  2768  3eqtr4i  2771  3eqtr4ri  2772  rabab  3503  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  5743  xpundir  5744  csbcnv  5882  resiun2  6001  resopab  6033  mptresid  6049  dffr3  6096  dfse2  6097  cnvun  6140  imaundir  6148  imainrect  6178  cnvcnv2  6190  cnvrescnv  6192  cnvcnvres  6202  dmtpop  6215  rnsnopg  6218  resdifdi  6233  rnco2  6250  dmco  6251  co01  6258  unidmrn  6276  dfdm2  6278  predidm  6325  tz6.26OLD  6347  dfmpt3  6682  mptun  6694  funcocnv2  6856  dffv2  6984  fnasrn  7140  fpr  7149  fmptap  7165  rnmptc  7205  rnmptcOLD  7206  riotav  7367  dmoprab  7507  rnoprab2  7510  mpov  7517  mpomptx  7518  abrexex2g  7948  1stval2  7989  2ndval2  7990  fo1st  7992  fo2nd  7993  xp2  8009  dfoprab4f  8039  offval22  8071  fmpoco  8078  fimaproj  8118  tposmpo  8245  tposconst  8246  recsfval  8378  rdgsucmpt2  8427  frsucmpt2  8437  df2o3  8471  o1p1e2  8537  o2p2e4  8538  oarec  8559  omopthlem2  8656  ecqs  8772  qliftf  8796  erovlem  8804  fset0  8845  mapsnf1o3  8886  ixp0x  8917  omf1o  9072  xpf1o  9136  mapunen  9143  enp1ilem  9275  pwfiOLD  9344  marypha1lem  9425  marypha2lem4  9430  dfoi  9503  infeq5i  9628  oemapso  9674  cantnflem1  9681  rankelop  9866  leweon  10003  r0weon  10004  kmlem11  10152  dju1dif  10164  ackbij1lem16  10227  cf0  10243  cfsmolem  10262  alephsuc3  10572  fpwwe  10638  canthp1lem1  10644  wuncval2  10739  prlem936  11039  m1p1sr  11084  m1m1sr  11085  dfcnqs  11134  ssxr  11280  mul02lem2  11388  addrid  11391  2p2e4  12344  3p2e5  12360  3p3e6  12361  4p2e6  12362  4p3e7  12363  4p4e8  12364  5p2e7  12365  5p3e8  12366  5p4e9  12367  6p2e8  12368  6p3e9  12369  7p2e9  12370  nnzrab  12587  nn0zrab  12588  dec0u  12695  dec0h  12696  decsuc  12705  decsucc  12715  numma  12718  decma  12725  decmac  12726  decma2c  12727  decadd  12728  decaddc  12729  decmul1c  12739  decmul2c  12740  5p5e10  12745  6p4e10  12746  7p3e10  12749  8p2e10  12754  5t5e25  12777  6t6e36  12782  8t6e48  12793  nn0uz  12861  nnuz  12862  xaddcom  13216  x2times  13275  ioomax  13396  iccmax  13397  ioopos  13398  ioorp  13399  prunioo  13455  fseq1p1m1  13572  fzo13pr  13713  fzo0to2pr  13714  fzo0to3tp  13715  om2uzrdg  13918  fzennn  13930  irec  14162  sq10e99m1  14222  facnn  14232  fac0  14233  faclbnd2  14248  faclbnd4lem1  14250  hashfun  14394  hashbclem  14408  hashf1lem1  14412  hashf1lem1OLD  14413  hashf1lem2  14414  fz1isolem  14419  swrdccatin1  14672  swrdccat3blem  14686  s1co  14781  s2eq2s1eq  14884  s3eqs2s1eq  14886  ofs2  14915  dfid5  14971  dfid6  14972  fsumrev2  15725  fsumparts  15749  fsumiun  15764  isumnn0nn  15785  harmonic  15802  fprod2d  15922  bpoly2  15998  bpoly3  15999  bpoly4  16000  ege2le3  16030  cos1bnd  16127  efieq1re  16139  eirrlem  16144  qnnen  16153  cpnnen  16169  ruclem6  16175  3dvds  16271  pwp1fsum  16331  m1bits  16378  algrp1  16508  phiprmpw  16706  prmreclem4  16849  4sqlem11  16885  4sqlem19  16893  dec5dvds  16994  decsplit1  17012  5prm  17039  7prm  17041  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  1259prm  17066  2503lem1  17067  2503lem2  17068  2503lem3  17069  2503prm  17070  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  4001prm  17075  strle1  17088  grpbasex  17233  grpplusgx  17234  quslem  17486  xpsrnbas  17514  acsfn1  17602  acsfn2  17604  comfffval2  17642  dfinito2  17950  dftermo2  17951  xpchomfval  18128  xpccofval  18131  1stfval  18140  2ndfval  18143  oduleg  18240  ismgmid  18581  efmndbas  18749  smndex2dnrinv  18793  grpinvfvi  18864  gaorb  19166  elcntr  19189  cntri  19191  cntrsubgnsg  19202  cntrnsg  19203  setsplusg  19209  oppglemOLD  19210  oppgcntr  19227  gsumwrev  19228  symgressbas  19244  symgplusg  19245  symgvalstruct  19259  symgvalstructOLD  19260  symgga  19270  cayleylem1  19275  psgnunilem2  19358  efgval2  19587  efgredlemc  19608  efgcpbllema  19617  frgpnabllem1  19736  gsumzaddlem  19784  mgplemOLD  19987  opprlem  20148  opprlemOLD  20149  oppr0  20156  opprneg  20158  rmodislmod  20533  rmodislmodOLD  20534  rlmscaf  20824  xrsds  20981  gsumfsum  21005  zringunit  21028  cnmsgngrp  21124  psgnfix2  21144  relt  21160  ocv0  21222  thlle  21243  thlleOLD  21244  thlleval  21245  dsmmval2  21283  frlmip  21325  mplbas  21541  mplplusg  21558  mplmulr  21559  mplvsca2  21565  ressmplbas2  21574  ltbwe  21591  evlslem4  21629  psr1bas2  21706  ply1bas  21711  ply1assa  21715  psr1plusg  21736  psr1vsca  21737  psr1mulr  21738  ply1plusg  21739  ply1vsca  21740  ply1mulr  21741  ply1mpl0  21769  ply1mpl1  21771  coe1mul  21784  matgsum  21931  smadiadetglem1  22165  indistpsx  22505  iuncld  22541  tgrest  22655  resstopn  22682  leordtval2  22708  xkouni  23095  ptclsg  23111  ptuncnv  23303  ptunhmeo  23304  alexsubALTlem4  23546  tsmsf1o  23641  ucnimalem  23777  ressxms  24026  uniretop  24271  cnfldtopn  24290  xrtgioo  24314  zcld  24321  icccmp  24333  xrge0gsumle  24341  xrge0tsms  24342  metnrmlem3  24369  fsum2cn  24379  cnmpopc  24436  oprpiece1res1  24459  oprpiece1res2  24460  evth  24467  evth2  24468  om1opn  24544  pi1xfrf  24561  pi1xfrcnv  24565  pi1cof  24567  clsocv  24759  cncmet  24831  cnflduss  24865  rrxprds  24898  ehlbase  24924  ismbl  25035  shftmbl  25047  ioorinv  25085  itg1addlem4  25208  itg1addlem4OLD  25209  itg2cnlem1  25271  itg0  25289  itgss3  25324  ditgneg  25366  limcdif  25385  limciun  25403  dvexp  25462  dvef  25489  dvcnvrelem2  25527  ftc1  25551  aannenlem2  25834  dvradcnv  25925  pserdvlem2  25932  reefgim  25954  cospi  25974  sincos6thpi  26017  tanregt0  26040  dflog2  26061  logfac  26101  dvlog  26151  cxpexp  26168  cxpmul2  26189  cxpsqrt  26203  dvsqrt  26240  dvcnsqrt  26242  cxpcn2  26244  isosctrlem2  26314  1cubrlem  26336  1cubr  26337  quart1lem  26350  atancj  26405  atanlogaddlem  26408  atansopn  26427  leibpilem2  26436  log2cnv  26439  log2ublem3  26443  birthdaylem1  26446  birthdaylem2  26447  birthday  26449  dfarea  26455  lgamgulmlem5  26527  lgambdd  26531  ftalem3  26569  basellem2  26576  ppiprm  26645  ppinprm  26646  chtprm  26647  chtnprm  26648  ppi2  26664  ppi3  26665  ppiub  26697  chtub  26705  bclbnd  26773  bposlem8  26784  lgsdilem  26817  lgsdir2lem2  26819  lgsquadlem2  26874  lgsquad2lem2  26878  2lgsoddprmlem3c  26905  rplogsum  27020  mulog2sumlem2  27028  pnt2  27106  bdayfo  27170  bday0s  27319  bday1s  27322  old1  27360  addsasslem2  27477  negsbdaylem  27520  muls01  27558  istrkg2ld  27701  axsegconlem9  28173  ax5seglem7  28183  iedgedg  28300  uspgrf1oedg  28423  nbgrcl  28582  nbgrnvtx0  28586  rusgrprc  28837  pthsfval  28968  wlkiswwlks2lem4  29116  wlkiswwlks2lem5  29117  clwwlkvbij  29356  konigsbergumgr  29494  ex-pw  29672  ex-xp  29679  ex-rn  29683  nvvop  29850  nvm  29882  cnims  29934  ip0i  30066  ip1ilem  30067  ipdirilem  30070  ipasslem10  30080  h2hva  30215  h2hsm  30216  h2hvs  30218  axhfvadd-zf  30223  axhvcom-zf  30224  axhvass-zf  30225  axhv0cl-zf  30226  axhvaddid-zf  30227  axhfvmul-zf  30228  axhvmulid-zf  30229  axhvmulass-zf  30230  axhvdistr1-zf  30231  axhvdistr2-zf  30232  axhvmul0-zf  30233  axhfi-zf  30234  axhis1-zf  30235  axhis2-zf  30236  axhis3-zf  30237  axhis4-zf  30238  axhcompl-zf  30239  normlem0  30350  normlem1  30351  normlem2  30352  normlem4  30354  normlem9  30359  bcseqi  30361  dfhnorm2  30363  norm3difi  30388  normpari  30395  normpar2i  30397  polid2i  30398  polidi  30399  hhba  30408  hhims  30413  hhims2  30414  hhsssh  30510  hhssims  30515  hhssims2  30516  shsval3i  30629  dfch2  30648  cmcm2i  30834  fh2  30860  qlaxr3i  30877  spansnji  30887  pjcji  30925  ho0val  30991  df0op2  30993  hosd1i  31063  hosd2i  31064  eigorthi  31078  hhlnoi  31141  hhnmoi  31142  hhbloi  31143  bra0  31191  nmop0  31227  nmfn0  31228  lnopeq0lem1  31246  lnopunilem1  31251  lnophmlem2  31258  nmopcoadji  31342  pjhmopidm  31424  cvmdi  31565  cdj3lem3  31679  cdj3lem3b  31681  abrexdomjm  31732  uniin1  31771  uniin2  31772  iundifdifd  31781  iundifdif  31782  mpomptxf  31893  df1stres  31913  df2ndres  31914  intimafv  31920  fcobijfs  31936  resf1o  31943  fpwrelmapffslem  31945  dpval3  32048  dp3mul10  32052  dpadd2  32064  dpmul4  32068  xrslt  32165  xrsclat  32169  xrge0tsmsd  32197  gsumle  32230  cycpmco2lem7  32279  cycpmconjv  32289  cycpmrn  32290  rndrhmcl  32385  xrge0slmod  32452  lsmsnorb2  32491  qusbas2  32506  rlmdim  32683  rgmoddimOLD  32684  circtopn  32806  tpr2rico  32881  xrge0mulc1cn  32910  lmxrge0  32921  esumpfinvallem  33061  esumcocn  33067  hasheuni  33072  esumcvg  33073  rossros  33167  measinblem  33207  aean  33231  sxbrsigalem3  33260  dya2iocival  33261  dya2iocucvr  33272  sxbrsigalem1  33273  sxbrsigalem2  33274  sxbrsigalem5  33276  sxbrsiga  33278  fiunelcarsg  33304  eulerpartlem1  33355  eulerpartgbij  33360  fibp1  33389  coinfliplem  33466  coinflipprob  33467  ballotlemfval  33477  ballotth  33525  sgnneg  33528  plymulx  33548  circlemethhgt  33644  hgt750lem2  33653  bnj1400  33835  bnj66  33860  bnj882  33926  lfuhgr  34097  derang0  34149  subfacp1lem1  34159  subfacp1lem6  34165  kur14lem7  34192  cvmsss2  34254  cvmliftlem8  34272  cvmliftlem10  34274  satfv1lem  34342  msubfval  34504  quad3  34644  bcprod  34697  bccolsum  34698  faclim  34705  pprodcnveq  34844  dfon4  34854  fobigcup  34861  dfiota3  34884  dfrecs2  34911  dfrdg4  34912  dfint3  34913  rankeq1o  35132  refssfne  35232  ssoninhaus  35322  onint1  35323  bj-rababw  35750  bj-inrab3  35798  bj-imdiridlem  36055  dissneq  36211  dffinxpf  36255  finxpreclem4  36264  rabiun  36450  ptrest  36476  poimirlem3  36480  poimirlem4  36481  poimirlem13  36490  poimirlem16  36493  poimirlem22  36499  poimirlem26  36503  poimirlem27  36504  poimirlem30  36507  cnambfre  36525  ftc1anclem8  36557  fnopabco  36580  abrexdom  36587  cncfres  36622  scottexf  37025  scott0f  37026  inres2  37101  dfres4  37151  xrnres  37261  xrnres2  37262  dfcoss2  37272  dfcoss4  37274  1cossres  37288  dmcoss2  37313  1cosscnvxrn  37334  dfeqvrels2  37447  dfcoeleqvrels  37480  redundss3  37487  dffunsALTV5  37546  cdleme3d  39091  cdleme7a  39103  cdleme31sdnN  39247  cdlemk45  39807  420gcd8e4  40860  lcmeprodgcdi  40861  60lcm7e420  40864  420lcm8e840  40865  3lexlogpow5ineq1  40908  3lexlogpow2ineq1  40912  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1p1  40930  2ap1caineq  40950  sticksstones7  40957  sticksstones12a  40962  sticksstones12  40963  imaopab  41048  fmpocos  41054  dfqs2  41057  dfqs3  41058  decaddcom  41194  sumcubes  41207  nn0expgcd  41222  sn-00idlem2  41269  reixi  41292  mapfzcons  41440  eldioph4b  41535  diophren  41537  pwssplit4  41817  pwfi2f1o  41824  frlmpwfi  41826  mendplusgfval  41913  mendmulrfval  41915  mendvscafval  41918  idomodle  41924  cytpval  41937  arearect  41950  onov0suclim  42010  omabs2  42068  tr3dom  42265  har2o  42283  alephiso2  42295  alephiso3  42296  relintab  42320  dfid7  42349  cnvrcl0  42362  dfrtrcl5  42366  dfrcl3  42412  dfrcl4  42413  comptiunov2i  42443  corcltrcl  42476  neicvgnvo  42852  inductionexd  42892  mnuprdlem2  43018  nznngen  43061  hashnzfz2  43066  lhe4.4ex1a  43074  dvradcnv2  43092  binomcxplemrat  43095  binomcxplemnotnn0  43101  refsum2cnlem1  43707  fiiuncl  43738  iccdifprioo  44216  lptre2pt  44343  limclner  44354  stoweidlem13  44716  stoweidlem32  44735  stoweidlem62  44765  wallispi2lem2  44775  stirlinglem14  44790  dirkertrigeqlem1  44801  dirkercncflem4  44809  fourierdlem42  44852  fourierdlem73  44882  fourierdlem81  44890  fourierdlem92  44901  fourierdlem103  44912  fourierdlem104  44913  fouriercnp  44929  fouriersw  44934  sge0tsms  45083  sge0iunmptlemfi  45116  ovolval5lem3  45357  cnfsmf  45443  rnfdmpr  45976  fvmptrabdm  45988  fundcmpsurinjlem1  46053  m11nprm  46256  opoeALTV  46338  nfermltl8rev  46397  sbgoldbo  46442  evengpop3  46453  cznabel  46806  cznrng  46807  mpomptx2  46964  2sphere  47389  itscnhlinecirc02plem3  47424  inlinecirc02p  47427  icccldii  47505  dfnrm2  47518  dfnrm3  47519  amgmlemALT  47804