Theorem eqtr4i 2647

Description: An equality transitivity inference. (Contributed by NM, 26-May-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	|- A = B
eqtr4i.2	|- C = B

Assertion

Ref	Expression
eqtr4i	|- A = C

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 |- A = B
2		eqtr4i.2	. . 3 |- C = B
3	2	eqcomi 2631	. 2 |- B = C
4	1, 3	eqtri 2644	1 |- A = C

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  3eqtr2i  2650  3eqtr2ri  2651  3eqtr4i  2654  3eqtr4ri  2655  rabab  3223  cbvralcsf  3565  cbvrabcsf  3568  dfin5  3582  dfdif2  3583  uneqin  3878  unrab  3898  inrab  3899  inrab2  3900  difrab  3901  dfrab3ss  3905  rabun2  3906  difidALT  3949  rabxm  3961  elnelun  3964  elnelunOLD  3966  difdifdir  4056  dfif3  4100  dfif5  4102  rabsnif  4258  tpidm  4293  ssunpr  4365  sstp  4367  dfint2  4477  iunrab  4567  uniiun  4573  intiin  4574  0iin  4578  mptv  4751  dfepfr  5099  epfrc  5100  xpundi  5171  xpundir  5172  csbcnv  5306  resiun2  5418  resopab  5446  opabresid  5455  dffr3  5498  dfse2  5499  cnvun  5538  imaundir  5546  imainrect  5575  cnvcnv2  5588  cnvcnvres  5598  dmtpop  5611  rnsnopg  5614  rnco2  5642  dmco  5643  co01  5650  unidmrn  5665  dfdm2  5667  predidm  5702  tz6.26  5711  dfmpt3  6014  mptun  6025  funcocnv2  6161  dffv2  6271  fnasrn  6411  fpr  6421  fmptap  6436  riotav  6616  dmoprab  6741  rnoprab2  6744  mpt2v  6750  mpt2mptx  6751  abrexex2g  7144  abrexex2OLD  7150  1stval2  7185  2ndval2  7186  fo1st  7188  fo2nd  7189  xp2  7203  dfoprab4f  7226  offval22  7253  fmpt2co  7260  tposmpt2  7389  tposconst  7390  recsfval  7477  rdgsucmpt2  7526  frsucmpt2  7535  df2o3  7573  o1p1e2  7620  o2p2e4  7621  oarec  7642  omopthlem2  7736  ecqs  7811  qliftf  7835  erovlem  7843  mapsnf1o3  7906  ixp0x  7936  omf1o  8063  xpf1o  8122  mapunen  8129  enp1ilem  8194  pwfi  8261  marypha1lem  8339  marypha2lem4  8344  dfoi  8416  infeq5i  8533  oemapso  8579  cantnflem1  8586  rankelop  8737  leweon  8834  r0weon  8835  kmlem11  8982  infcda1  9015  ackbij1lem16  9057  cf0  9073  cfsmolem  9092  alephsuc3  9402  fpwwe  9468  canthp1lem1  9474  wuncval2  9569  prlem936  9869  m1p1sr  9913  m1m1sr  9914  dfcnqs  9963  ssxr  10107  mul02lem2  10213  addid1  10216  2p2e4  11144  3p2e5  11160  3p3e6  11161  4p2e6  11162  4p3e7  11163  4p4e8  11164  5p2e7  11165  5p3e8  11166  5p4e9  11167  5p5e10OLD  11168  6p2e8  11169  6p3e9  11170  6p4e10OLD  11171  7p2e9  11172  7p3e10OLD  11173  8p2e10OLD  11174  nnzrab  11405  nn0zrab  11406  dec0u  11520  dec0uOLD  11521  dec0h  11522  dec0hOLD  11523  decsuc  11535  decsucOLD  11536  decsucc  11550  decsuccOLD  11551  numma  11557  decma  11564  decmaOLD  11565  decmac  11566  decmacOLD  11567  decma2c  11568  decma2cOLD  11569  decadd  11570  decaddOLD  11571  decaddc  11572  decaddcOLD  11573  decmul1  11585  decmul1OLD  11586  decmul1c  11587  decmul1cOLD  11588  decmul2c  11589  decmul2cOLD  11590  5p5e10  11596  6p4e10  11598  7p3e10  11603  8p2e10  11610  5t5e25  11639  5t5e25OLD  11640  6t6e36  11646  6t6e36OLD  11647  8t6e48  11659  8t6e48OLD  11660  nn0uz  11722  nnuz  11723  xaddcom  12071  x2times  12129  ioomax  12248  iccmax  12249  ioopos  12250  ioorp  12251  prunioo  12301  fseq1p1m1  12414  fzo13pr  12552  fzo0to2pr  12553  fzo0to3tp  12554  om2uzrdg  12755  fzennn  12767  irec  12964  sq10e99m1  13049  sq10e99m1OLD  13052  facnn  13062  fac0  13063  faclbnd2  13078  faclbnd4lem1  13080  hashfun  13224  hashbclem  13236  hashf1lem1  13239  hashf1lem2  13240  fz1isolem  13245  swrdccatin1  13483  swrdccat3blem  13495  s1co  13579  s2eq2s1eq  13681  s3eqs2s1eq  13683  ofs2  13710  dfid5  13767  dfid6  13768  fsumrev2  14514  fsumparts  14538  fsumiun  14553  isumnn0nn  14574  harmonic  14591  0.999...OLD  14613  fprod2d  14711  bpoly2  14788  bpoly3  14789  bpoly4  14790  ege2le3  14820  cos1bnd  14917  efieq1re  14929  eirrlem  14932  qnnen  14942  cpnnen  14958  ruclem6  14964  3dvds  15052  3dvdsOLD  15053  pwp1fsum  15114  m1bits  15162  algrp1  15287  phiprmpw  15481  prmreclem4  15623  4sqlem11  15659  4sqlem19  15667  dec5dvds  15768  decsplit1  15786  decsplit1OLD  15790  5prm  15815  7prm  15817  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  ndxidOLD  15884  strle1  15973  grpbasex  15994  grpplusgx  15995  quslem  16203  xpslem  16233  acsfn1  16322  acsfn2  16324  comfffval2  16361  xpchomfval  16819  xpccofval  16822  1stfval  16831  2ndfval  16834  oduleg  17132  ismgmid  17264  grpinvfvi  17463  gaorb  17740  cntri  17763  cntrsubgnsg  17773  cntrnsg  17774  oppglem  17780  oppgcntr  17795  gsumwrev  17796  symgbas  17800  symgga  17826  cayleylem1  17832  psgnunilem2  17915  efgval2  18137  efgredlemc  18158  efgcpbllema  18167  frgpnabllem1  18276  gsumzaddlem  18321  mgplem  18494  opprlem  18628  oppr0  18633  opprneg  18635  rmodislmod  18931  rlmscaf  19208  mplbas  19429  mpladd  19442  mplmul  19443  mplvsca2  19446  ressmplbas2  19455  ltbwe  19472  evlslem4  19508  psr1bas2  19560  ply1bas  19565  ply1assa  19569  mplplusg  19590  mplmulr  19591  psr1plusg  19592  psr1vsca  19593  psr1mulr  19594  ply1plusg  19595  ply1vsca  19596  ply1mulr  19597  ply1mpl0  19625  ply1mpl1  19627  coe1mul  19640  xrsds  19789  gsumfsum  19813  zringunit  19836  cnmsgngrp  19925  psgnfix2  19945  relt  19961  ocv0  20021  thlle  20041  thlleval  20042  dsmmval2  20080  frlmip  20117  matgsum  20243  smadiadetglem1  20477  indistpsx  20814  iuncld  20849  tgrest  20963  resstopn  20990  leordtval2  21016  xkouni  21402  ptclsg  21418  ptuncnv  21610  ptunhmeo  21611  alexsubALTlem4  21854  tsmsf1o  21948  ucnimalem  22084  ressxms  22330  uniretop  22566  cnfldtopn  22585  xrtgioo  22609  zcld  22616  icccmp  22628  xrge0gsumle  22636  xrge0tsms  22637  metnrmlem3  22664  fsum2cn  22674  cnmpt2pc  22727  oprpiece1res1  22750  oprpiece1res2  22751  evth  22758  evth2  22759  om1opn  22836  pi1xfrf  22853  pi1xfrcnv  22857  pi1cof  22859  clsocv  23049  cncmet  23119  cnflduss  23152  rrxprds  23177  ehlbase  23194  ismbl  23294  shftmbl  23306  ioorinv  23344  itg1addlem4  23466  itg2cnlem1  23528  iblitg  23535  itg0  23546  itgss3  23581  ditgneg  23621  limcdif  23640  limciun  23658  dvexp  23716  dvef  23743  dvcnvrelem2  23781  ftc1  23805  plyremlem  24059  aannenlem2  24084  taylply2  24122  dvradcnv  24175  pserdvlem2  24182  reefgim  24204  cospi  24224  sincos6thpi  24267  tanregt0  24285  dflog2  24307  logfac  24347  dvlog  24397  cxpexp  24414  cxpmul2  24435  cxpsqrt  24449  dvsqrt  24483  dvcnsqrt  24485  cxpcn2  24487  ang180lem2  24540  isosctrlem2  24549  1cubrlem  24568  1cubr  24569  quart1lem  24582  atancj  24637  atanlogaddlem  24640  atansopn  24659  leibpilem2  24668  log2cnv  24671  log2ublem3  24675  birthdaylem1  24678  birthdaylem2  24679  birthday  24681  dfarea  24687  lgamgulmlem5  24759  lgambdd  24763  wilthlem2  24795  ftalem3  24801  ftalem7  24805  basellem2  24808  ppiprm  24877  ppinprm  24878  chtprm  24879  chtnprm  24880  ppi2  24896  ppi3  24897  ppiub  24929  chtub  24937  bclbnd  25005  bposlem8  25016  lgsdilem  25049  lgsdir2lem1  25050  lgsdir2lem2  25051  lgsdir2lem3  25052  lgsquadlem2  25106  lgsquad2lem2  25110  2lgsoddprmlem3c  25137  rplogsum  25216  mulog2sumlem2  25224  pnt2  25302  istrkg2ld  25359  axsegconlem9  25805  ax5seglem7  25815  iedgedg  25943  uspgrf1oedg  26068  nbgrnvtx0  26237  rusgrprc  26486  wlkiswwlks2lem4  26758  wlkiswwlks2lem5  26759  wwlksnfi  26801  wlksnwwlknvbij  26803  clwwlksvbij  26922  konigsbergumgr  27112  konigsbergupgrOLD  27113  ex-pw  27286  ex-xp  27293  ex-rn  27297  nvvop  27464  nvm  27496  cnims  27548  ip0i  27680  ip1ilem  27681  ipdirilem  27684  ipasslem10  27694  h2hva  27831  h2hsm  27832  h2hvs  27834  axhfvadd-zf  27839  axhvcom-zf  27840  axhvass-zf  27841  axhv0cl-zf  27842  axhvaddid-zf  27843  axhfvmul-zf  27844  axhvmulid-zf  27845  axhvmulass-zf  27846  axhvdistr1-zf  27847  axhvdistr2-zf  27848  axhvmul0-zf  27849  axhfi-zf  27850  axhis1-zf  27851  axhis2-zf  27852  axhis3-zf  27853  axhis4-zf  27854  axhcompl-zf  27855  normlem0  27966  normlem1  27967  normlem2  27968  normlem4  27970  normlem9  27975  bcseqi  27977  dfhnorm2  27979  norm3difi  28004  normpari  28011  normpar2i  28013  polid2i  28014  polidi  28015  hhba  28024  hhims  28029  hhims2  28030  hhsssh  28126  hhssims  28132  hhssims2  28133  shsval3i  28247  dfch2  28266  cmcm2i  28452  fh2  28478  qlaxr3i  28495  spansnji  28505  pjcji  28543  ho0val  28609  df0op2  28611  hosd1i  28681  hosd2i  28682  eigorthi  28696  hhlnoi  28759  hhnmoi  28760  hhbloi  28761  bra0  28809  nmop0  28845  nmfn0  28846  lnopeq0lem1  28864  lnopunilem1  28869  lnophmlem2  28876  nmopcoadji  28960  pjhmopidm  29042  cvmdi  29183  cdj3lem3  29297  cdj3lem3b  29299  abrexdomjm  29345  uniin1  29367  uniin2  29368  iundifdifd  29380  iundifdif  29381  mpt2mptxf  29477  df1stres  29481  df2ndres  29482  fcobijfs  29501  resf1o  29505  fpwrelmapffslem  29507  dpval3  29602  dp3mul10  29606  dpadd2  29618  dpmul4  29622  xrslt  29676  xrsclat  29680  gsumle  29779  xrge0tsmsd  29785  xrge0slmod  29844  fimaproj  29900  circtopn  29904  tpr2rico  29958  xrge0mulc1cn  29987  lmxrge0  29998  esumpfinvallem  30136  esumcocn  30142  hasheuni  30147  esumcvg  30148  rossros  30243  measinblem  30283  aean  30307  sxbrsigalem3  30334  dya2iocival  30335  dya2iocucvr  30346  sxbrsigalem1  30347  sxbrsigalem2  30348  sxbrsigalem5  30350  sxbrsiga  30352  fiunelcarsg  30378  eulerpartlem1  30429  eulerpartgbij  30434  fibp1  30463  coinfliplem  30540  coinflipprob  30541  ballotlemfval  30551  ballotth  30599  sgnneg  30602  plymulx  30625  circlemethhgt  30721  hgt750lem2  30730  bnj1400  30906  bnj66  30930  bnj882  30996  derang0  31151  subfacp1lem1  31161  subfacp1lem6  31167  kur14lem7  31194  cvmsss2  31256  cvmliftlem8  31274  cvmliftlem10  31276  msubfval  31421  quad3  31564  bcprod  31624  bccolsum  31625  faclim  31632  dftrpred2  31719  bdayfo  31828  pprodcnveq  31990  dfon4  32000  fobigcup  32007  dfiota3  32030  dfrecs2  32057  dfrdg4  32058  dfint3  32059  rankeq1o  32278  refssfne  32353  ssoninhaus  32447  onint1  32448  bj-rababwv  32867  bj-inrab3  32925  rnmptsn  33182  dissneq  33188  dffinxpf  33222  finxpreclem4  33231  rabiun  33382  ptrest  33408  poimirlem3  33412  poimirlem4  33413  poimirlem13  33422  poimirlem16  33425  poimirlem22  33431  poimirlem26  33435  poimirlem27  33436  poimirlem30  33439  cnambfre  33458  ftc1anclem8  33492  fnopabco  33517  abrexdom  33525  cncfres  33564  scottexf  33976  scott0f  33977  inres2  34007  dfres4  34061  opidORIG  34109  cdleme3d  35518  cdleme7a  35530  cdleme31sdnN  35675  cdlemk45  36235  mapfzcons  37279  eldioph4b  37375  diophren  37377  pwssplit4  37659  pwfi2f1o  37666  frlmpwfi  37668  mendplusgfval  37755  mendmulrfval  37757  mendvscafval  37760  idomodle  37774  cytpval  37787  arearect  37801  relintab  37889  dfid7  37919  cnvrcl0  37932  dfrtrcl5  37936  dfrcl3  37967  dfrcl4  37968  comptiunov2i  37998  corcltrcl  38031  neicvgnvo  38413  inductionexd  38453  nznngen  38515  hashnzfz2  38520  lhe4.4ex1a  38528  dvradcnv2  38546  binomcxplemrat  38549  binomcxplemnotnn0  38555  compneOLD  38644  refsum2cnlem1  39196  fiiuncl  39234  rnmptc  39353  iccdifprioo  39742  lptre2pt  39872  limclner  39883  stoweidlem13  40230  stoweidlem32  40249  stoweidlem62  40279  wallispi2lem2  40289  stirlinglem14  40304  dirkertrigeqlem1  40315  dirkercncflem4  40323  fourierdlem42  40366  fourierdlem73  40396  fourierdlem81  40404  fourierdlem92  40415  fourierdlem103  40426  fourierdlem104  40427  fouriercnp  40443  fouriersw  40448  sge0tsms  40597  sge0iunmptlemfi  40630  ovolval5lem3  40868  cnfsmf  40949  rnfdmpr  41300  m11nprm  41518  opoeALTV  41594  sbgoldbo  41675  evengpop3  41686  cznabel  41954  cznrng  41955  mpt2mptx2  42113  amgmlemALT  42549