MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr4i Structured version   Visualization version   GIF version

Theorem eqtr4i 2850
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
StepHypRef Expression
1 eqtr4i.1 . 2 𝐴 = 𝐵
2 eqtr4i.2 . . 3 𝐶 = 𝐵
32eqcomi 2833 . 2 𝐵 = 𝐶
41, 3eqtri 2847 1 𝐴 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817
This theorem is referenced by:  3eqtr2i  2853  3eqtr2ri  2854  3eqtr4i  2857  3eqtr4ri  2858  rabab  3509  cbvralcsf  3908  cbvrabcsf  3911  dfin5  3927  dfdif2  3928  uneqin  4240  unrab  4259  inrab  4260  inrab2  4261  difrab  4262  dfrab3ss  4266  rabun2  4267  difidALT  4314  rabxm  4323  elnelun  4326  difdifdir  4420  dfif3  4464  dfif5  4466  rabsnif  4644  tpidm  4679  ssunpr  4749  sstp  4751  opidg  4808  dfint2  4864  iunrab  4962  uniiun  4968  intiin  4969  0iin  4973  mptv  5157  dfepfr  5527  epfrc  5528  xpundi  5607  xpundir  5608  csbcnv  5741  resiun2  5861  resopab  5889  mptresid  5905  opabresidOLD  5906  dffr3  5949  dfse2  5950  cnvun  5988  imaundir  5996  imainrect  6025  cnvcnv2  6037  cnvrescnv  6039  cnvcnvres  6049  dmtpop  6062  rnsnopg  6065  rnco2  6093  dmco  6094  co01  6101  unidmrn  6117  dfdm2  6119  predidm  6157  tz6.26  6166  dfmpt3  6471  mptun  6483  funcocnv2  6630  dffv2  6747  fnasrn  6898  fpr  6907  fmptap  6923  rnmptc  6960  rnmptcOLD  6961  riotav  7112  dmoprab  7248  rnoprab2  7251  mpov  7257  mpomptx  7258  abrexex2g  7660  1stval2  7701  2ndval2  7702  fo1st  7704  fo2nd  7705  xp2  7721  dfoprab4f  7749  offval22  7779  fmpoco  7786  fimaproj  7825  tposmpo  7925  tposconst  7926  recsfval  8013  rdgsucmpt2  8062  frsucmpt2w  8071  frsucmpt2  8072  df2o3  8113  o1p1e2  8161  o2p2e4  8162  o2p2e4OLD  8163  oarec  8184  omopthlem2  8279  ecqs  8357  qliftf  8381  erovlem  8389  mapsnf1o3  8455  ixp0x  8486  omf1o  8616  xpf1o  8676  mapunen  8683  enp1ilem  8749  pwfi  8816  marypha1lem  8894  marypha2lem4  8899  dfoi  8972  infeq5i  9096  oemapso  9142  cantnflem1  9149  rankelop  9300  leweon  9435  r0weon  9436  kmlem11  9584  dju1dif  9596  ackbij1lem16  9655  cf0  9671  cfsmolem  9690  alephsuc3  10000  fpwwe  10066  canthp1lem1  10072  wuncval2  10167  prlem936  10467  m1p1sr  10512  m1m1sr  10513  dfcnqs  10562  ssxr  10708  mul02lem2  10815  addid1  10818  2p2e4  11769  3p2e5  11785  3p3e6  11786  4p2e6  11787  4p3e7  11788  4p4e8  11789  5p2e7  11790  5p3e8  11791  5p4e9  11792  6p2e8  11793  6p3e9  11794  7p2e9  11795  nnzrab  12007  nn0zrab  12008  dec0u  12116  dec0h  12117  decsuc  12126  decsucc  12136  numma  12139  decma  12146  decmac  12147  decma2c  12148  decadd  12149  decaddc  12150  decmul1c  12160  decmul2c  12161  5p5e10  12166  6p4e10  12167  7p3e10  12170  8p2e10  12175  5t5e25  12198  6t6e36  12203  8t6e48  12214  nn0uz  12277  nnuz  12278  xaddcom  12630  x2times  12689  ioomax  12809  iccmax  12810  ioopos  12811  ioorp  12812  prunioo  12868  fseq1p1m1  12985  fzo13pr  13125  fzo0to2pr  13126  fzo0to3tp  13127  om2uzrdg  13328  fzennn  13340  irec  13569  sq10e99m1  13630  facnn  13640  fac0  13641  faclbnd2  13656  faclbnd4lem1  13658  hashfun  13803  hashbclem  13815  hashf1lem1  13818  hashf1lem2  13819  fz1isolem  13824  swrdccatin1  14087  swrdccat3blem  14101  s1co  14195  s2eq2s1eq  14298  s3eqs2s1eq  14300  ofs2  14331  dfid5  14386  dfid6  14387  fsumrev2  15137  fsumparts  15161  fsumiun  15176  isumnn0nn  15197  harmonic  15214  fprod2d  15335  bpoly2  15411  bpoly3  15412  bpoly4  15413  ege2le3  15443  cos1bnd  15540  efieq1re  15552  eirrlem  15557  qnnen  15566  cpnnen  15582  ruclem6  15588  3dvds  15680  pwp1fsum  15740  m1bits  15787  algrp1  15916  phiprmpw  16111  prmreclem4  16253  4sqlem11  16289  4sqlem19  16297  dec5dvds  16398  decsplit1  16416  5prm  16442  7prm  16444  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  strle1  16592  grpbasex  16613  grpplusgx  16614  quslem  16816  xpsrnbas  16844  acsfn1  16932  acsfn2  16934  comfffval2  16971  xpchomfval  17429  xpccofval  17432  1stfval  17441  2ndfval  17444  oduleg  17742  ismgmid  17875  efmndbas  18036  smndex2dnrinv  18080  grpinvfvi  18146  gaorb  18437  cntri  18461  cntrsubgnsg  18471  cntrnsg  18472  oppglem  18478  oppgcntr  18493  gsumwrev  18494  symgressbas  18510  symgplusg  18511  symgvalstruct  18525  symgga  18535  cayleylem1  18540  psgnunilem2  18623  efgval2  18850  efgredlemc  18871  efgcpbllema  18880  frgpnabllem1  18993  gsumzaddlem  19041  mgplem  19244  opprlem  19381  oppr0  19386  opprneg  19388  rmodislmod  19702  rlmscaf  19981  mplbas  20209  mpladd  20222  mplmul  20223  mplvsca2  20226  ressmplbas2  20236  ltbwe  20253  evlslem4  20288  psr1bas2  20358  ply1bas  20363  ply1assa  20367  mplplusg  20388  mplmulr  20389  psr1plusg  20390  psr1vsca  20391  psr1mulr  20392  ply1plusg  20393  ply1vsca  20394  ply1mulr  20395  ply1mpl0  20423  ply1mpl1  20425  coe1mul  20438  xrsds  20588  gsumfsum  20612  zringunit  20635  cnmsgngrp  20723  psgnfix2  20743  relt  20759  ocv0  20821  thlle  20841  thlleval  20842  dsmmval2  20880  frlmip  20922  matgsum  21046  smadiadetglem1  21280  indistpsx  21618  iuncld  21653  tgrest  21767  resstopn  21794  leordtval2  21820  xkouni  22207  ptclsg  22223  ptuncnv  22415  ptunhmeo  22416  alexsubALTlem4  22658  tsmsf1o  22753  ucnimalem  22889  ressxms  23135  uniretop  23371  cnfldtopn  23390  xrtgioo  23414  zcld  23421  icccmp  23433  xrge0gsumle  23441  xrge0tsms  23442  metnrmlem3  23469  fsum2cn  23479  cnmpopc  23536  oprpiece1res1  23559  oprpiece1res2  23560  evth  23567  evth2  23568  om1opn  23644  pi1xfrf  23661  pi1xfrcnv  23665  pi1cof  23667  clsocv  23857  cncmet  23929  cnflduss  23963  rrxprds  23996  ehlbase  24022  ismbl  24133  shftmbl  24145  ioorinv  24183  itg1addlem4  24306  itg2cnlem1  24368  itg0  24386  itgss3  24421  ditgneg  24463  limcdif  24482  limciun  24500  dvexp  24559  dvef  24586  dvcnvrelem2  24624  ftc1  24648  aannenlem2  24928  dvradcnv  25019  pserdvlem2  25026  reefgim  25048  cospi  25068  sincos6thpi  25111  tanregt0  25134  dflog2  25155  logfac  25195  dvlog  25245  cxpexp  25262  cxpmul2  25283  cxpsqrt  25297  dvsqrt  25334  dvcnsqrt  25336  cxpcn2  25338  isosctrlem2  25408  1cubrlem  25430  1cubr  25431  quart1lem  25444  atancj  25499  atanlogaddlem  25502  atansopn  25521  leibpilem2  25530  log2cnv  25533  log2ublem3  25537  birthdaylem1  25540  birthdaylem2  25541  birthday  25543  dfarea  25549  lgamgulmlem5  25621  lgambdd  25625  ftalem3  25663  basellem2  25670  ppiprm  25739  ppinprm  25740  chtprm  25741  chtnprm  25742  ppi2  25758  ppi3  25759  ppiub  25791  chtub  25799  bclbnd  25867  bposlem8  25878  lgsdilem  25911  lgsdir2lem2  25913  lgsquadlem2  25968  lgsquad2lem2  25972  2lgsoddprmlem3c  25999  rplogsum  26114  mulog2sumlem2  26122  pnt2  26200  istrkg2ld  26257  axsegconlem9  26722  ax5seglem7  26732  iedgedg  26846  uspgrf1oedg  26969  nbgrcl  27128  nbgrnvtx0  27132  rusgrprc  27383  wlkiswwlks2lem4  27661  wlkiswwlks2lem5  27662  clwwlkvbij  27901  konigsbergumgr  28039  ex-pw  28217  ex-xp  28224  ex-rn  28228  nvvop  28395  nvm  28427  cnims  28479  ip0i  28611  ip1ilem  28612  ipdirilem  28615  ipasslem10  28625  h2hva  28760  h2hsm  28761  h2hvs  28763  axhfvadd-zf  28768  axhvcom-zf  28769  axhvass-zf  28770  axhv0cl-zf  28771  axhvaddid-zf  28772  axhfvmul-zf  28773  axhvmulid-zf  28774  axhvmulass-zf  28775  axhvdistr1-zf  28776  axhvdistr2-zf  28777  axhvmul0-zf  28778  axhfi-zf  28779  axhis1-zf  28780  axhis2-zf  28781  axhis3-zf  28782  axhis4-zf  28783  axhcompl-zf  28784  normlem0  28895  normlem1  28896  normlem2  28897  normlem4  28899  normlem9  28904  bcseqi  28906  dfhnorm2  28908  norm3difi  28933  normpari  28940  normpar2i  28942  polid2i  28943  polidi  28944  hhba  28953  hhims  28958  hhims2  28959  hhsssh  29055  hhssims  29060  hhssims2  29061  shsval3i  29174  dfch2  29193  cmcm2i  29379  fh2  29405  qlaxr3i  29422  spansnji  29432  pjcji  29470  ho0val  29536  df0op2  29538  hosd1i  29608  hosd2i  29609  eigorthi  29623  hhlnoi  29686  hhnmoi  29687  hhbloi  29688  bra0  29736  nmop0  29772  nmfn0  29773  lnopeq0lem1  29791  lnopunilem1  29796  lnophmlem2  29803  nmopcoadji  29887  pjhmopidm  29969  cvmdi  30110  cdj3lem3  30224  cdj3lem3b  30226  abrexdomjm  30277  uniin1  30314  uniin2  30315  iundifdifd  30324  iundifdif  30325  mpomptxf  30436  df1stres  30450  df2ndres  30451  fcobijfs  30470  resf1o  30477  fpwrelmapffslem  30479  dpval3  30581  dp3mul10  30585  dpadd2  30597  dpmul4  30601  xrslt  30695  xrsclat  30699  xrge0tsmsd  30724  gsumle  30757  cycpmco2lem7  30806  cycpmconjv  30816  cycpmrn  30817  xrge0slmod  30950  rgmoddim  31068  circtopn  31161  tpr2rico  31212  xrge0mulc1cn  31241  lmxrge0  31252  esumpfinvallem  31390  esumcocn  31396  hasheuni  31401  esumcvg  31402  rossros  31496  measinblem  31536  aean  31560  sxbrsigalem3  31587  dya2iocival  31588  dya2iocucvr  31599  sxbrsigalem1  31600  sxbrsigalem2  31601  sxbrsigalem5  31603  sxbrsiga  31605  fiunelcarsg  31631  eulerpartlem1  31682  eulerpartgbij  31687  fibp1  31716  coinfliplem  31793  coinflipprob  31794  ballotlemfval  31804  ballotth  31852  sgnneg  31855  plymulx  31875  circlemethhgt  31971  hgt750lem2  31980  bnj1400  32164  bnj66  32189  bnj882  32255  lfuhgr  32421  derang0  32473  subfacp1lem1  32483  subfacp1lem6  32489  kur14lem7  32516  cvmsss2  32578  cvmliftlem8  32596  cvmliftlem10  32598  satfv1lem  32666  msubfval  32828  quad3  32970  bcprod  33027  bccolsum  33028  faclim  33035  dftrpred2  33115  bdayfo  33239  pprodcnveq  33401  dfon4  33411  fobigcup  33418  dfiota3  33441  dfrecs2  33468  dfrdg4  33469  dfint3  33470  rankeq1o  33689  refssfne  33763  ssoninhaus  33853  onint1  33854  bj-rababw  34265  bj-inrab3  34315  bj-imdiridlem  34545  dissneq  34703  dffinxpf  34747  finxpreclem4  34756  wl-dfrabsb  34971  rabiun  34975  ptrest  35001  poimirlem3  35005  poimirlem4  35006  poimirlem13  35015  poimirlem16  35018  poimirlem22  35024  poimirlem26  35028  poimirlem27  35029  poimirlem30  35032  cnambfre  35050  ftc1anclem8  35082  fnopabco  35106  abrexdom  35113  cncfres  35148  scottexf  35551  scott0f  35552  inres2  35611  dfres4  35655  xrnres  35755  xrnres2  35756  dfcoss2  35766  dfcoss4  35768  1cossres  35779  dmcoss2  35799  1cosscnvxrn  35820  dfeqvrels2  35928  dfcoeleqvrels  35961  redundss3  35968  dffunsALTV5  36025  cdleme3d  37472  cdleme7a  37484  cdleme31sdnN  37628  cdlemk45  38188  420gcd8e4  39242  lcmeprodgcdi  39243  60lcm7e420  39246  420lcm8e840  39247  3lexlogpow5ineq1  39289  2ap1caineq  39295  imaopab  39347  dfqs2  39350  dfqs3  39351  decaddcom  39408  nn0expgcd  39422  sn-00idlem2  39467  reixi  39489  mapfzcons  39573  eldioph4b  39668  diophren  39670  pwssplit4  39949  pwfi2f1o  39956  frlmpwfi  39958  mendplusgfval  40045  mendmulrfval  40047  mendvscafval  40050  idomodle  40056  cytpval  40069  arearect  40081  tr3dom  40152  alephiso2  40173  alephiso3  40174  relintab  40199  dfid7  40228  cnvrcl0  40241  dfrtrcl5  40245  dfrcl3  40292  dfrcl4  40293  comptiunov2i  40323  corcltrcl  40356  neicvgnvo  40737  inductionexd  40777  mnuprdlem2  40901  nznngen  40940  hashnzfz2  40945  lhe4.4ex1a  40953  dvradcnv2  40971  binomcxplemrat  40974  binomcxplemnotnn0  40980  refsum2cnlem1  41586  fiiuncl  41619  iccdifprioo  42079  lptre2pt  42208  limclner  42219  stoweidlem13  42581  stoweidlem32  42600  stoweidlem62  42630  wallispi2lem2  42640  stirlinglem14  42655  dirkertrigeqlem1  42666  dirkercncflem4  42674  fourierdlem42  42717  fourierdlem73  42747  fourierdlem81  42755  fourierdlem92  42766  fourierdlem103  42777  fourierdlem104  42778  fouriercnp  42794  fouriersw  42799  sge0tsms  42945  sge0iunmptlemfi  42978  ovolval5lem3  43219  cnfsmf  43300  rnfdmpr  43763  fvmptrabdm  43775  fundcmpsurinjlem1  43841  m11nprm  44045  opoeALTV  44127  nfermltl8rev  44186  sbgoldbo  44231  evengpop3  44242  cznabel  44504  cznrng  44505  mpomptx2  44662  2sphere  45089  itscnhlinecirc02plem3  45124  inlinecirc02p  45127  amgmlemALT  45257
  Copyright terms: Public domain W3C validator