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

Theorem eqtr4i 2844
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 2827 . 2 𝐵 = 𝐶
41, 3eqtri 2841 1 𝐴 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  3eqtr2i  2847  3eqtr2ri  2848  3eqtr4i  2851  3eqtr4ri  2852  rabab  3521  cbvralcsf  3922  cbvrabcsf  3925  dfin5  3941  dfdif2  3942  uneqin  4252  unrab  4271  inrab  4272  inrab2  4273  difrab  4274  dfrab3ss  4278  rabun2  4279  difidALT  4328  rabxm  4337  elnelun  4340  difdifdir  4433  dfif3  4477  dfif5  4479  rabsnif  4651  tpidm  4686  ssunpr  4757  sstp  4759  opidg  4814  dfint2  4869  iunrab  4967  uniiun  4973  intiin  4974  0iin  4978  mptv  5162  dfepfr  5533  epfrc  5534  xpundi  5613  xpundir  5614  csbcnv  5747  resiun2  5867  resopab  5895  mptresid  5911  opabresidOLD  5912  dffr3  5955  dfse2  5956  cnvun  5994  imaundir  6002  imainrect  6031  cnvcnv2  6043  cnvrescnv  6045  cnvcnvres  6055  dmtpop  6068  rnsnopg  6071  rnco2  6099  dmco  6100  co01  6107  unidmrn  6123  dfdm2  6125  predidm  6163  tz6.26  6172  dfmpt3  6475  mptun  6487  funcocnv2  6632  dffv2  6749  fnasrn  6899  fpr  6908  fmptap  6924  rnmptc  6961  riotav  7108  dmoprab  7244  rnoprab2  7247  mpov  7253  mpomptx  7254  abrexex2g  7654  1stval2  7695  2ndval2  7696  fo1st  7698  fo2nd  7699  xp2  7715  dfoprab4f  7743  offval22  7772  fmpoco  7779  fimaproj  7818  tposmpo  7918  tposconst  7919  recsfval  8006  rdgsucmpt2  8055  frsucmpt2w  8064  frsucmpt2  8065  df2o3  8106  o1p1e2  8154  o2p2e4  8155  o2p2e4OLD  8156  oarec  8177  omopthlem2  8272  ecqs  8350  qliftf  8374  erovlem  8382  mapsnf1o3  8447  ixp0x  8478  omf1o  8608  xpf1o  8667  mapunen  8674  enp1ilem  8740  pwfi  8807  marypha1lem  8885  marypha2lem4  8890  dfoi  8963  infeq5i  9087  oemapso  9133  cantnflem1  9140  rankelop  9291  leweon  9425  r0weon  9426  kmlem11  9574  dju1dif  9586  ackbij1lem16  9645  cf0  9661  cfsmolem  9680  alephsuc3  9990  fpwwe  10056  canthp1lem1  10062  wuncval2  10157  prlem936  10457  m1p1sr  10502  m1m1sr  10503  dfcnqs  10552  ssxr  10698  mul02lem2  10805  addid1  10808  2p2e4  11760  3p2e5  11776  3p3e6  11777  4p2e6  11778  4p3e7  11779  4p4e8  11780  5p2e7  11781  5p3e8  11782  5p4e9  11783  6p2e8  11784  6p3e9  11785  7p2e9  11786  nnzrab  11998  nn0zrab  11999  dec0u  12107  dec0h  12108  decsuc  12117  decsucc  12127  numma  12130  decma  12137  decmac  12138  decma2c  12139  decadd  12140  decaddc  12141  decmul1c  12151  decmul2c  12152  5p5e10  12157  6p4e10  12158  7p3e10  12161  8p2e10  12166  5t5e25  12189  6t6e36  12194  8t6e48  12205  nn0uz  12268  nnuz  12269  xaddcom  12621  x2times  12680  ioomax  12799  iccmax  12800  ioopos  12801  ioorp  12802  prunioo  12855  fseq1p1m1  12969  fzo13pr  13109  fzo0to2pr  13110  fzo0to3tp  13111  om2uzrdg  13312  fzennn  13324  irec  13552  sq10e99m1  13613  facnn  13623  fac0  13624  faclbnd2  13639  faclbnd4lem1  13641  hashfun  13786  hashbclem  13798  hashf1lem1  13801  hashf1lem2  13802  fz1isolem  13807  swrdccatin1  14075  swrdccat3blem  14089  s1co  14183  s2eq2s1eq  14286  s3eqs2s1eq  14288  ofs2  14319  dfid5  14374  dfid6  14375  fsumrev2  15125  fsumparts  15149  fsumiun  15164  isumnn0nn  15185  harmonic  15202  fprod2d  15323  bpoly2  15399  bpoly3  15400  bpoly4  15401  ege2le3  15431  cos1bnd  15528  efieq1re  15540  eirrlem  15545  qnnen  15554  cpnnen  15570  ruclem6  15576  3dvds  15668  pwp1fsum  15730  m1bits  15777  algrp1  15906  phiprmpw  16101  prmreclem4  16243  4sqlem11  16279  4sqlem19  16287  dec5dvds  16388  decsplit1  16406  5prm  16430  7prm  16432  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  1259prm  16457  2503lem1  16458  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  4001prm  16466  strle1  16580  grpbasex  16601  grpplusgx  16602  quslem  16804  xpsrnbas  16832  acsfn1  16920  acsfn2  16922  comfffval2  16959  xpchomfval  17417  xpccofval  17420  1stfval  17429  2ndfval  17432  oduleg  17730  ismgmid  17863  grpinvfvi  18084  gaorb  18375  cntri  18399  cntrsubgnsg  18409  cntrnsg  18410  oppglem  18416  oppgcntr  18431  gsumwrev  18432  symgbas  18436  symgga  18464  cayleylem1  18469  psgnunilem2  18552  efgval2  18779  efgredlemc  18800  efgcpbllema  18809  frgpnabllem1  18922  gsumzaddlem  18970  mgplem  19173  opprlem  19307  oppr0  19312  opprneg  19314  rmodislmod  19631  rlmscaf  19909  mplbas  20137  mpladd  20150  mplmul  20151  mplvsca2  20154  ressmplbas2  20164  ltbwe  20181  evlslem4  20216  psr1bas2  20286  ply1bas  20291  ply1assa  20295  mplplusg  20316  mplmulr  20317  psr1plusg  20318  psr1vsca  20319  psr1mulr  20320  ply1plusg  20321  ply1vsca  20322  ply1mulr  20323  ply1mpl0  20351  ply1mpl1  20353  coe1mul  20366  xrsds  20516  gsumfsum  20540  zringunit  20563  cnmsgngrp  20651  psgnfix2  20671  relt  20687  ocv0  20749  thlle  20769  thlleval  20770  dsmmval2  20808  frlmip  20850  matgsum  20974  smadiadetglem1  21208  indistpsx  21546  iuncld  21581  tgrest  21695  resstopn  21722  leordtval2  21748  xkouni  22135  ptclsg  22151  ptuncnv  22343  ptunhmeo  22344  alexsubALTlem4  22586  tsmsf1o  22680  ucnimalem  22816  ressxms  23062  uniretop  23298  cnfldtopn  23317  xrtgioo  23341  zcld  23348  icccmp  23360  xrge0gsumle  23368  xrge0tsms  23369  metnrmlem3  23396  fsum2cn  23406  cnmpopc  23459  oprpiece1res1  23482  oprpiece1res2  23483  evth  23490  evth2  23491  om1opn  23567  pi1xfrf  23584  pi1xfrcnv  23588  pi1cof  23590  clsocv  23780  cncmet  23852  cnflduss  23886  rrxprds  23919  ehlbase  23945  ismbl  24054  shftmbl  24066  ioorinv  24104  itg1addlem4  24227  itg2cnlem1  24289  itg0  24307  itgss3  24342  ditgneg  24382  limcdif  24401  limciun  24419  dvexp  24477  dvef  24504  dvcnvrelem2  24542  ftc1  24566  aannenlem2  24845  dvradcnv  24936  pserdvlem2  24943  reefgim  24965  cospi  24985  sincos6thpi  25028  tanregt0  25050  dflog2  25071  logfac  25111  dvlog  25161  cxpexp  25178  cxpmul2  25199  cxpsqrt  25213  dvsqrt  25250  dvcnsqrt  25252  cxpcn2  25254  isosctrlem2  25324  1cubrlem  25346  1cubr  25347  quart1lem  25360  atancj  25415  atanlogaddlem  25418  atansopn  25437  leibpilem2  25446  log2cnv  25449  log2ublem3  25453  birthdaylem1  25456  birthdaylem2  25457  birthday  25459  dfarea  25465  lgamgulmlem5  25537  lgambdd  25541  ftalem3  25579  basellem2  25586  ppiprm  25655  ppinprm  25656  chtprm  25657  chtnprm  25658  ppi2  25674  ppi3  25675  ppiub  25707  chtub  25715  bclbnd  25783  bposlem8  25794  lgsdilem  25827  lgsdir2lem2  25829  lgsquadlem2  25884  lgsquad2lem2  25888  2lgsoddprmlem3c  25915  rplogsum  26030  mulog2sumlem2  26038  pnt2  26116  istrkg2ld  26173  axsegconlem9  26638  ax5seglem7  26648  iedgedg  26762  uspgrf1oedg  26885  nbgrcl  27044  nbgrnvtx0  27048  rusgrprc  27299  wlkiswwlks2lem4  27577  wlkiswwlks2lem5  27578  wwlksnfiOLD  27612  clwwlkvbij  27819  konigsbergumgr  27957  ex-pw  28135  ex-xp  28142  ex-rn  28146  nvvop  28313  nvm  28345  cnims  28397  ip0i  28529  ip1ilem  28530  ipdirilem  28533  ipasslem10  28543  h2hva  28678  h2hsm  28679  h2hvs  28681  axhfvadd-zf  28686  axhvcom-zf  28687  axhvass-zf  28688  axhv0cl-zf  28689  axhvaddid-zf  28690  axhfvmul-zf  28691  axhvmulid-zf  28692  axhvmulass-zf  28693  axhvdistr1-zf  28694  axhvdistr2-zf  28695  axhvmul0-zf  28696  axhfi-zf  28697  axhis1-zf  28698  axhis2-zf  28699  axhis3-zf  28700  axhis4-zf  28701  axhcompl-zf  28702  normlem0  28813  normlem1  28814  normlem2  28815  normlem4  28817  normlem9  28822  bcseqi  28824  dfhnorm2  28826  norm3difi  28851  normpari  28858  normpar2i  28860  polid2i  28861  polidi  28862  hhba  28871  hhims  28876  hhims2  28877  hhsssh  28973  hhssims  28978  hhssims2  28979  shsval3i  29092  dfch2  29111  cmcm2i  29297  fh2  29323  qlaxr3i  29340  spansnji  29350  pjcji  29388  ho0val  29454  df0op2  29456  hosd1i  29526  hosd2i  29527  eigorthi  29541  hhlnoi  29604  hhnmoi  29605  hhbloi  29606  bra0  29654  nmop0  29690  nmfn0  29691  lnopeq0lem1  29709  lnopunilem1  29714  lnophmlem2  29721  nmopcoadji  29805  pjhmopidm  29887  cvmdi  30028  cdj3lem3  30142  cdj3lem3b  30144  abrexdomjm  30194  uniin1  30230  uniin2  30231  iundifdifd  30241  iundifdif  30242  mpomptxf  30353  df1stres  30365  df2ndres  30366  fcobijfs  30385  resf1o  30392  fpwrelmapffslem  30394  dpval3  30497  dp3mul10  30501  dpadd2  30513  dpmul4  30517  xrslt  30590  xrsclat  30594  xrge0tsmsd  30619  gsumle  30652  cycpmco2lem7  30701  cycpmconjv  30711  cycpmrn  30712  xrge0slmod  30844  rgmoddim  30907  circtopn  31000  tpr2rico  31054  xrge0mulc1cn  31083  lmxrge0  31094  esumpfinvallem  31232  esumcocn  31238  hasheuni  31243  esumcvg  31244  rossros  31338  measinblem  31378  aean  31402  sxbrsigalem3  31429  dya2iocival  31430  dya2iocucvr  31441  sxbrsigalem1  31442  sxbrsigalem2  31443  sxbrsigalem5  31445  sxbrsiga  31447  fiunelcarsg  31473  eulerpartlem1  31524  eulerpartgbij  31529  fibp1  31558  coinfliplem  31635  coinflipprob  31636  ballotlemfval  31646  ballotth  31694  sgnneg  31697  plymulx  31717  circlemethhgt  31813  hgt750lem2  31822  bnj1400  32006  bnj66  32031  bnj882  32097  lfuhgr  32261  derang0  32313  subfacp1lem1  32323  subfacp1lem6  32329  kur14lem7  32356  cvmsss2  32418  cvmliftlem8  32436  cvmliftlem10  32438  satfv1lem  32506  msubfval  32668  quad3  32810  bcprod  32867  bccolsum  32868  faclim  32875  dftrpred2  32955  bdayfo  33079  pprodcnveq  33241  dfon4  33251  fobigcup  33258  dfiota3  33281  dfrecs2  33308  dfrdg4  33309  dfint3  33310  rankeq1o  33529  refssfne  33603  ssoninhaus  33693  onint1  33694  bj-rababw  34094  bj-inrab3  34144  dissneq  34504  dffinxpf  34548  finxpreclem4  34557  wl-dfrabsb  34742  rabiun  34746  ptrest  34772  poimirlem3  34776  poimirlem4  34777  poimirlem13  34786  poimirlem16  34789  poimirlem22  34795  poimirlem26  34799  poimirlem27  34800  poimirlem30  34803  cnambfre  34821  ftc1anclem8  34855  fnopabco  34879  abrexdom  34886  cncfres  34924  scottexf  35327  scott0f  35328  inres2  35387  dfres4  35431  xrnres  35530  xrnres2  35531  dfcoss2  35541  dfcoss4  35543  1cossres  35554  dmcoss2  35574  1cosscnvxrn  35595  dfeqvrels2  35703  dfcoeleqvrels  35736  redundss3  35743  dffunsALTV5  35800  cdleme3d  37247  cdleme7a  37259  cdleme31sdnN  37403  cdlemk45  37963  imaopab  38997  dfqs2  39000  dfqs3  39001  decaddcom  39048  nn0expgcd  39062  sn-00idlem2  39107  mapfzcons  39191  eldioph4b  39286  diophren  39288  pwssplit4  39567  pwfi2f1o  39574  frlmpwfi  39576  mendplusgfval  39663  mendmulrfval  39665  mendvscafval  39668  idomodle  39674  cytpval  39687  arearect  39700  tr3dom  39772  alephiso2  39795  alephiso3  39796  relintab  39821  dfid7  39850  cnvrcl0  39863  dfrtrcl5  39867  dfrcl3  39898  dfrcl4  39899  comptiunov2i  39929  corcltrcl  39962  neicvgnvo  40343  inductionexd  40383  mnuprdlem2  40486  nznngen  40525  hashnzfz2  40530  lhe4.4ex1a  40538  dvradcnv2  40556  binomcxplemrat  40559  binomcxplemnotnn0  40565  refsum2cnlem1  41171  fiiuncl  41204  iccdifprioo  41668  lptre2pt  41797  limclner  41808  stoweidlem13  42175  stoweidlem32  42194  stoweidlem62  42224  wallispi2lem2  42234  stirlinglem14  42249  dirkertrigeqlem1  42260  dirkercncflem4  42268  fourierdlem42  42311  fourierdlem73  42341  fourierdlem81  42349  fourierdlem92  42360  fourierdlem103  42371  fourierdlem104  42372  fouriercnp  42388  fouriersw  42393  sge0tsms  42539  sge0iunmptlemfi  42572  ovolval5lem3  42813  cnfsmf  42894  rnfdmpr  43357  fvmptrabdm  43369  fundcmpsurinjlem1  43435  m11nprm  43643  opoeALTV  43725  nfermltl8rev  43784  sbgoldbo  43829  evengpop3  43840  efmndbas  43970  smndex2dnrinv  44015  cznabel  44153  cznrng  44154  mpomptx2  44311  2sphere  44664  itscnhlinecirc02plem3  44699  inlinecirc02p  44702  amgmlemALT  44832
  Copyright terms: Public domain W3C validator