Theorem eqtr4i 2792

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  3eqtr2i  2795  3eqtr2ri  2796  3eqtr4i  2799  3eqtr4ri  2800  rabab  3488  cbvralcsf  3898  cbvrabcsf  3901  dfin5  3916  dfdif2  3917  uneqin  4245  notabw  4269  unrab  4271  inrab  4272  inrab2  4273  difrab  4274  dfrab3ss  4279  rabun2  4280  dfnul2  4292  difid  4335  rabxm  4350  elnelun  4353  abf  4374  difdifdir  4455  dfif3  4505  dfif5  4507  rabsnif  4692  tpidm  4727  ssunpr  4802  sstp  4804  opidg  4860  dfint2  4917  iunrab  5020  uniiun  5026  intiin  5027  iunid  5028  0iin  5031  uniin1  5042  uniin2  5043  mptv  5220  dfepfr  5648  epfrc  5649  xpundi  5733  xpundir  5734  csbcnv  5875  csbcnvOLD  5876  resiun2  6002  resopab  6039  mptresid  6056  dffr3  6104  dfse2  6105  cnvun  6142  imaundir  6151  imainrect  6182  cnvcnv2  6194  cnvrescnv  6197  cnvcnvres  6209  dmtpop  6222  rnsnopg  6225  resdifdi  6240  rnco2  6258  dmco  6259  co01  6266  unidmrn  6284  dfdm2  6286  predidm  6331  dfmpt3  6673  mptun  6685  funcocnv2  6850  dffv2  6980  fnasrn  7145  fpr  7155  fmptap  7172  rnmptc  7209  riotav  7378  dmoprab  7519  rnoprab2  7522  mpov  7528  mpomptx  7529  abrexex2g  7963  1stval2  8005  2ndval2  8006  fo1st  8008  fo2nd  8009  xp2  8025  dfoprab4f  8055  offval22  8085  fmpoco  8092  fimaproj  8133  tposmpo  8261  tposconst  8262  recsfval  8369  rdgsucmpt2  8419  frsucmpt2  8429  df2o3  8463  o1p1e2  8527  o2p2e4  8528  oarec  8549  omopthlem2  8648  dfqs2  8703  ecqs  8779  qliftf  8805  erovlem  8813  fset0  8853  mapsnf1o3  8895  ixp0x  8926  omf1o  9070  xpf1o  9129  mapunen  9136  enp1ilem  9240  marypha1lem  9395  marypha2lem4  9400  dfoi  9475  infeq5i  9607  oemapso  9653  cantnflem1  9660  rankelop  9848  leweon  10006  r0weon  10007  kmlem11  10155  dju1dif  10167  ackbij1lem16  10228  cf0  10244  cfsmolem  10264  alephsuc3  10575  fpwwe  10641  canthp1lem1  10647  wuncval2  10742  prlem936  11042  m1p1sr  11087  m1m1sr  11088  dfcnqs  11137  ssxr  11289  mul02lem2  11397  addrid  11400  2p2e4  12385  3p2e5  12401  3p3e6  12402  4p2e6  12403  4p3e7  12404  4p4e8  12405  5p2e7  12406  5p3e8  12407  5p4e9  12408  6p2e8  12409  6p3e9  12410  7p2e9  12411  nnzrab  12632  nn0zrab  12633  dec0u  12747  dec0h  12748  decsuc  12757  decsucc  12767  numma  12770  decma  12777  decmac  12778  decma2c  12779  decadd  12780  decaddc  12781  decmul1c  12791  decmul2c  12792  5p5e10  12797  6p4e10  12798  7p3e10  12801  8p2e10  12806  5t5e25  12829  6t6e36  12834  8t6e48  12845  nn0uz  12910  nnuz  12911  xaddcom  13276  x2times  13335  ioomax  13459  iccmax  13460  ioopos  13461  ioorp  13462  prunioo  13518  fseq1p1m1  13637  fzo13pr  13789  fzo0to2pr  13790  fzo0to3tp  13792  om2uzrdg  14003  fzennn  14015  irec  14248  sq10e99m1  14312  facnn  14322  fac0  14323  faclbnd2  14338  faclbnd4lem1  14340  hashfun  14485  hashbclem  14500  hashf1lem1  14503  hashf1lem2  14504  fz1isolem  14509  swrdccatin1  14773  swrdccat3blem  14787  s1co  14881  s2eq2s1eq  14984  s3eqs2s1eq  14986  ofs2  15019  dfid5  15075  dfid6  15076  sgnneg  15148  fsumrev2  15844  fsumparts  15869  fsumiun  15884  isumnn0nn  15907  harmonic  15924  fprod2d  16046  bpoly2  16121  bpoly3  16122  bpoly4  16123  ege2le3  16154  cos1bnd  16253  efieq1re  16265  eirrlem  16270  qnnen  16279  cpnnen  16295  ruclem6  16301  3dvds  16399  pwp1fsum  16459  m1bits  16508  nn0expgcd  16632  algrp1  16642  phiprmpw  16845  prmreclem4  16989  4sqlem11  17025  4sqlem19  17033  dec5dvds  17134  decsplit1  17151  5prm  17178  7prm  17180  1259lem2  17202  1259lem3  17203  1259lem4  17204  1259lem5  17205  1259prm  17206  2503lem1  17207  2503lem2  17208  2503lem3  17209  2503prm  17210  4001lem1  17211  4001lem2  17212  4001lem3  17213  4001lem4  17214  4001prm  17215  strle1  17228  grpbasex  17355  grpplusgx  17356  quslem  17607  xpsrnbas  17635  acsfn1  17727  acsfn2  17729  comfffval2  17767  dfinito2  18070  dftermo2  18071  xpchomfval  18245  xpccofval  18248  1stfval  18257  2ndfval  18260  oduleg  18356  chnub  18688  ismgmid  18733  efmndbas  18940  smndex2dnrinv  18987  grpinvfvi  19059  gaorb  19387  elcntr  19410  cntri  19412  cntrsubgnsg  19423  cntrnsg  19424  setsplusg  19430  oppgcntr  19445  gsumwrev  19446  symgressbas  19462  symgplusg  19463  symgvalstruct  19477  symgga  19487  cayleylem1  19492  psgnunilem2  19575  efgval2  19804  efgredlemc  19825  efgcpbllema  19834  frgpnabllem1  19953  gsumzaddlem  20001  gsumle  20225  opprlem  20435  oppr0  20442  opprneg  20444  rmodislmod  21066  rlmscaf  21343  xrsds  21575  gsumfsum  21599  zringunit  21631  pzriprng1  21663  cnmsgngrp  21744  psgnfix2  21764  relt  21780  ocv0  21842  thlle  21862  thlleval  21863  dsmmval2  21901  frlmip  21943  mplbas  22154  mplplusg  22171  mplmulr  22172  mplvsca2  22178  ressmplbas2  22192  ltbwe  22210  evlslem4  22242  psdmul  22344  psr1bas2  22365  ply1bas  22370  ply1assa  22374  psr1plusg  22395  psr1vsca  22396  psr1mulr  22397  ply1plusg  22398  ply1vsca  22399  ply1mulr  22400  ply1mpl0  22431  ply1mpl1  22433  coe1mul  22446  matgsum  22609  smadiadetglem1  22843  indistpsx  23182  iuncld  23217  tgrest  23331  resstopn  23358  leordtval2  23384  xkouni  23771  ptclsg  23787  ptuncnv  23979  ptunhmeo  23980  alexsubALTlem4  24222  tsmsf1o  24317  ucnimalem  24451  ressxms  24697  uniretop  24934  cnfldtopn  24953  xrtgioo  24979  zcld  24986  icccmp  24998  xrge0gsumle  25006  xrge0tsms  25007  metnrmlem3  25034  fsum2cn  25045  cnmpopc  25102  oprpiece1res1  25125  oprpiece1res2  25126  evth  25133  evth2  25134  om1opn  25210  pi1xfrf  25227  pi1xfrcnv  25231  pi1cof  25233  clsocv  25424  cncmet  25496  cnflduss  25530  rrxprds  25563  ehlbase  25589  ismbl  25700  shftmbl  25712  ioorinv  25750  itg1addlem4  25873  itg2cnlem1  25935  itg0  25954  itgss3  25989  ditgneg  26031  limcdif  26050  limciun  26068  dvexp  26127  dvef  26154  dvcnvrelem2  26192  ftc1  26216  plymulidp  26458  aannenlem2  26507  dvradcnv  26599  pserdvlem2  26606  reefgim  26628  cospi  26652  sincos6thpi  26696  tanregt0  26719  dflog2  26740  logfac  26781  dvlog  26831  cxpexp  26848  cxpmul2  26869  cxpsqrt  26883  dvsqrt  26922  dvcnsqrt  26924  cxpcn2  26926  isosctrlem2  26999  1cubrlem  27021  1cubr  27022  quart1lem  27035  atancj  27090  atanlogaddlem  27093  atansopn  27112  leibpilem2  27121  log2cnv  27124  log2ublem3  27128  birthdaylem1  27131  birthdaylem2  27132  birthday  27134  dfarea  27140  lgamgulmlem5  27212  lgambdd  27216  ftalem3  27254  basellem2  27261  ppiprm  27330  ppinprm  27331  chtprm  27332  chtnprm  27333  ppi2  27349  ppi3  27350  ppiub  27383  chtub  27391  bclbnd  27459  bposlem8  27470  lgsdilem  27503  lgsdir2lem2  27505  lgsquadlem2  27560  lgsquad2lem2  27564  2lgsoddprmlem3c  27591  rplogsum  27706  mulog2sumlem2  27714  pnt2  27792  bdayfo  27856  bday0  28019  bday1  28022  old1  28073  addsasslem2  28212  negbdaylem  28264  muls01  28320  abssnid  28451  1p1e2s  28624  n0seo  28629  twocut  28631  halfcut  28666  pw2cutp1  28669  pw2cut2  28670  istrkg2ld  28744  axsegconlem9  29290  ax5seglem7  29300  iedgedg  29415  uspgrf1oedg  29538  nbgrcl  29700  nbgrnvtx0  29704  rusgrprc  29955  pthsfval  30083  wlkiswwlks2lem4  30236  wlkiswwlks2lem5  30237  clwwlkvbij  30479  konigsbergumgr  30617  ex-pw  30795  ex-xp  30802  ex-rn  30806  nvvop  30976  nvm  31008  cnims  31060  ip0i  31192  ip1ilem  31193  ipdirilem  31196  ipasslem10  31206  h2hva  31341  h2hsm  31342  h2hvs  31344  axhfvadd-zf  31349  axhvcom-zf  31350  axhvass-zf  31351  axhv0cl-zf  31352  axhvaddid-zf  31353  axhfvmul-zf  31354  axhvmulid-zf  31355  axhvmulass-zf  31356  axhvdistr1-zf  31357  axhvdistr2-zf  31358  axhvmul0-zf  31359  axhfi-zf  31360  axhis1-zf  31361  axhis2-zf  31362  axhis3-zf  31363  axhis4-zf  31364  axhcompl-zf  31365  normlem0  31476  normlem1  31477  normlem2  31478  normlem4  31480  normlem9  31485  bcseqi  31487  dfhnorm2  31489  norm3difi  31514  normpari  31521  normpar2i  31523  polid2i  31524  polidi  31525  hhba  31534  hhims  31539  hhims2  31540  hhsssh  31636  hhssims  31641  hhssims2  31642  shsval3i  31755  dfch2  31774  cmcm2i  31960  fh2  31986  qlaxr3i  32003  spansnji  32013  pjcji  32051  ho0val  32117  df0op2  32119  hosd1i  32189  hosd2i  32190  eigorthi  32204  hhlnoi  32267  hhnmoi  32268  hhbloi  32269  bra0  32317  nmop0  32353  nmfn0  32354  lnopeq0lem1  32372  lnopunilem1  32377  lnophmlem2  32384  nmopcoadji  32468  pjhmopidm  32550  cvmdi  32691  cdj3lem3  32805  cdj3lem3b  32807  abrexdomjm  32868  iundifdifd  32921  iundifdif  32922  mpomptxf  33038  df1stres  33064  df2ndres  33065  intimafv  33071  fcobijfs  33081  fcobijfs2  33082  resf1o  33090  fpwrelmapffslem  33092  dpval3  33228  dp3mul10  33232  dpadd2  33244  dpmul4  33248  ccatws1f1o  33284  xrslt  33340  xrsclat  33344  xrge0tsmsd  33406  cycpmco2lem7  33465  cycpmconjv  33475  cycpmrn  33476  conjga  33503  elrgspnsubrunlem2  33581  rndrhmcl  33630  fracf1  33641  xrge0slmod  33681  lsmsnorb2  33718  qusbas2  33728  1arithidomlem2  33839  zringfrac  33857  selvply1rhm0  33929  mplvrpmga  33948  mplvrpmmhm  33949  mplvrpmrhm  33950  psrmonprod  33955  mplmonprod  33957  vieta  33983  rlmdim  34013  isconstr  34139  iconstr  34169  cos9thpiminplylem4  34188  cos9thpiminplylem5  34189  circtopn  34240  tpr2rico  34315  xrge0mulc1cn  34344  lmxrge0  34355  esumpfinvallem  34477  esumcocn  34483  hasheuni  34488  esumcvg  34489  rossros  34583  measinblem  34623  aean  34647  sxbrsigalem3  34675  dya2iocival  34676  dya2iocucvr  34687  sxbrsigalem1  34688  sxbrsigalem2  34689  sxbrsigalem5  34691  sxbrsiga  34693  fiunelcarsg  34719  eulerpartlem1  34770  eulerpartgbij  34775  fibp1  34804  coinfliplem  34882  coinflipprob  34883  ballotlemfval  34893  ballotth  34941  circlemethhgt  35043  hgt750lem2  35052  bnj1400  35236  bnj66  35261  bnj882  35327  dfscott2  35524  dfscott3  35525  lfuhgr  35622  derang0  35673  subfacp1lem1  35683  subfacp1lem6  35689  kur14lem7  35716  cvmsss2  35778  cvmliftlem8  35796  cvmliftlem10  35798  satfv1lem  35866  msubfval  36028  quad3  36174  bcprod  36242  bccolsum  36243  faclim  36250  pprodcnveq  36385  dfon4  36395  fobigcup  36402  dfiota3  36425  dfrecs2  36454  dfrdg4  36455  dfint3  36456  rankeq1o  36675  refssfne  36901  ssoninhaus  36991  onint1  36992  ttciun  37057  bj-dfnul2  37195  bj-rababw  37548  bj-inrab3  37597  bj-imdiridlem  37861  dissneq  38019  dffinxpf  38063  finxpreclem4  38072  rabiun  38276  ptrest  38302  poimirlem3  38306  poimirlem4  38307  poimirlem13  38316  poimirlem16  38319  poimirlem22  38325  poimirlem26  38329  poimirlem27  38330  poimirlem30  38333  cnambfre  38351  ftc1anclem8  38383  fnopabco  38406  abrexdom  38413  cncfres  38448  scottexf  38849  scott0f  38850  inres2  38928  eqrabi  38937  xpv  38943  dfres4  38980  dmxrn  39068  xrnres  39106  xrnres2  39107  rnqmap  39135  dfsucmap2  39145  dfcoss2  39184  dfcoss4  39186  1cossres  39200  dmcoss2  39225  1cosscnvxrn  39246  dfeqvrels2  39353  dfcoeleqvrels  39386  redundss3  39393  dffunsALTV5  39453  dfpeters2  39655  cdleme3d  41037  cdleme7a  41049  cdleme31sdnN  41193  cdlemk45  41753  420gcd8e4  42805  lcmeprodgcdi  42806  60lcm7e420  42809  420lcm8e840  42810  3lexlogpow5ineq1  42853  3lexlogpow2ineq1  42857  3lexlogpow2ineq2  42858  3lexlogpow5ineq5  42859  aks4d1p1  42875  posbezout  42899  aks6d1c1p4  42910  aks6d1c3  42922  2ap1caineq  42944  sticksstones7  42951  sticksstones12a  42956  sticksstones12  42957  aks6d1c6lem4  42972  25or6to4  43005  imaopab  43034  fmpocos  43036  dfqs3  43039  decaddcom  43077  sumcubes  43106  redvmptabs  43153  readvrec  43155  readvcot  43157  sn-00idlem2  43192  reixi  43216  sum9cubes  43436  mapfzcons  43479  eldioph4b  43570  diophren  43572  pwssplit4  43848  pwfi2f1o  43855  frlmpwfi  43857  mendplusgfval  43940  mendmulrfval  43942  mendvscafval  43945  idomodle  43950  cytpval  43961  arearect  43974  onov0suclim  44033  omabs2  44091  tr3dom  44286  har2o  44304  alephiso2  44316  alephiso3  44317  relintab  44341  dfid7  44370  cnvrcl0  44383  dfrtrcl5  44387  dfrcl3  44433  dfrcl4  44434  comptiunov2i  44464  corcltrcl  44497  neicvgnvo  44873  inductionexd  44913  mnuprdlem2  45015  nznngen  45058  hashnzfz2  45063  lhe4.4ex1a  45071  dvradcnv2  45089  binomcxplemrat  45092  binomcxplemnotnn0  45098  nregmodelf1o  45756  refsum2cnlem1  45789  fiiuncl  45817  iccdifprioo  46264  lptre2pt  46386  limclner  46397  stoweidlem13  46759  stoweidlem32  46778  stoweidlem62  46808  wallispi2lem2  46818  stirlinglem14  46833  dirkertrigeqlem1  46844  dirkercncflem4  46852  fourierdlem42  46895  fourierdlem73  46925  fourierdlem81  46933  fourierdlem92  46944  fourierdlem103  46955  fourierdlem104  46956  fouriercnp  46972  fouriersw  46977  sge0tsms  47126  sge0iunmptlemfi  47159  ovolval5lem3  47400  cnfsmf  47486  lamberte  47657  rnfdmpr  48050  fvmptrabdm  48062  fundcmpsurinjlem1  48179  m11nprm  48385  ppi1sum  48415  opoeALTV  48480  nfermltl8rev  48539  sbgoldbo  48584  evengpop3  48595  clnbgrcl  48618  clnbgrnvtx0  48624  usgrexmpl2edg  48826  usgrexmpl2nb0  48828  usgrexmpl2nb3  48831  gpg5order  48857  gpgprismgr4cycllem6  48897  cznabel  49057  cznrng  49058  mpomptx2  49147  2sphere  49561  itscnhlinecirc02plem3  49596  inlinecirc02p  49599  dftpos5  49684  tposresg  49688  icccldii  49729  dfnrm2  49742  dfnrm3  49743  elxpcbasex1ALT  50059  elxpcbasex2ALT  50061  dfswapf2  50071  swapf1a  50079  swapf1f1o  50085  swapf2f1oa  50087  swapfida  50090  setc1oterm  50301  setc1ohomfval  50303  setc1ocofval  50304  funcsetc1o  50307  dfinito4  50311  setc1onsubc  50412  islmd  50475  iscmd  50476  initocmd  50479  termolmd  50480  amgmlemALT  50682