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

Theorem eqtr4i 2634
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 2618 . 2 𝐵 = 𝐶
41, 3eqtri 2631 1 𝐴 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  3eqtr2i  2637  3eqtr2ri  2638  3eqtr4i  2641  3eqtr4ri  2642  rabab  3195  cbvralcsf  3530  cbvrabcsf  3533  dfin5  3547  dfdif2  3548  uneqin  3836  unrab  3856  inrab  3857  inrab2  3858  difrab  3859  dfrab3ss  3863  rabun2  3864  difidALT  3902  rabxm  3914  elnelun  3917  difdifdir  4007  dfif3  4049  dfif5  4051  rabsnif  4201  tpidm  4236  ssunpr  4300  sstp  4302  dfint2  4406  iunrab  4497  uniiun  4503  intiin  4504  0iin  4508  mptv  4673  dfepfr  5013  epfrc  5014  xpundi  5084  xpundir  5085  csbcnv  5216  resiun2  5325  resopab  5353  opabresid  5361  dffr3  5404  dfse2  5405  cnvun  5443  imaundir  5451  imainrect  5480  cnvcnv2  5492  cnvcnvres  5502  dmtpop  5515  rnsnopg  5518  rnco2  5545  dmco  5546  co01  5553  unidmrn  5568  dfdm2  5570  predidm  5605  tz6.26  5614  dfmpt3  5913  mptun  5924  funcocnv2  6059  dffv2  6166  fnasrn  6302  fpr  6304  fmptap  6319  riotav  6494  dmoprab  6617  rnoprab2  6620  mpt2v  6626  mpt2mptx  6627  abrexex2g  7013  abrexex2  7017  1stval2  7053  2ndval2  7054  fo1st  7056  fo2nd  7057  xp2  7071  dfoprab4f  7094  offval22  7117  fmpt2co  7124  tposmpt2  7253  tposconst  7254  recsfval  7341  rdgsucmpt2  7390  frsucmpt2  7399  df2o3  7437  o1p1e2  7484  o2p2e4  7485  oarec  7506  omopthlem2  7600  ecqs  7675  qliftf  7699  erovlem  7707  mapsnf1o3  7769  ixp0x  7799  omf1o  7925  xpf1o  7984  mapunen  7991  enp1ilem  8056  pwfi  8121  marypha1lem  8199  marypha2lem4  8204  dfoi  8276  infeq5i  8393  oemapso  8439  cantnflem1  8446  rankelop  8597  leweon  8694  r0weon  8695  kmlem11  8842  infcda1  8875  ackbij1lem16  8917  cf0  8933  cfsmolem  8952  alephsuc3  9258  fpwwe  9324  canthp1lem1  9330  wuncval2  9425  prlem936  9725  m1p1sr  9769  m1m1sr  9770  dfcnqs  9819  ssxr  9958  mul02lem2  10064  addid1  10067  2p2e4  10991  3p2e5  11007  3p3e6  11008  4p2e6  11009  4p3e7  11010  4p4e8  11011  5p2e7  11012  5p3e8  11013  5p4e9  11014  5p5e10OLD  11015  6p2e8  11016  6p3e9  11017  6p4e10OLD  11018  7p2e9  11019  7p3e10OLD  11020  8p2e10OLD  11021  nnzrab  11238  nn0zrab  11239  dec0u  11352  dec0uOLD  11353  dec0h  11354  dec0hOLD  11355  decsuc  11367  decsucOLD  11368  decsucc  11382  decsuccOLD  11383  numma  11389  decma  11396  decmaOLD  11397  decmac  11398  decmacOLD  11399  decma2c  11400  decma2cOLD  11401  decadd  11402  decaddOLD  11403  decaddc  11404  decaddcOLD  11405  decmul1  11417  decmul1OLD  11418  decmul1c  11419  decmul1cOLD  11420  decmul2c  11421  decmul2cOLD  11422  5p5e10  11428  6p4e10  11430  7p3e10  11435  8p2e10  11442  5t5e25  11471  5t5e25OLD  11472  6t6e36  11478  6t6e36OLD  11479  8t6e48  11491  8t6e48OLD  11492  nn0uz  11554  nnuz  11555  xaddcom  11903  x2times  11958  ioomax  12075  iccmax  12076  ioopos  12077  ioorp  12078  prunioo  12128  fseq1p1m1  12238  fzo13pr  12374  fzo0to2pr  12375  fzo0to3tp  12376  om2uzrdg  12572  fzennn  12584  irec  12781  sq10e99m1  12866  sq10e99m1OLD  12869  facnn  12879  fac0  12880  faclbnd2  12895  faclbnd4lem1  12897  hashfun  13036  hashbclem  13045  hashf1lem1  13048  hashf1lem2  13049  fz1isolem  13054  swrdccatin1  13280  swrdccat3blem  13292  s1co  13376  s2eq2s1eq  13477  ofs2  13504  dfid5  13561  dfid6  13562  fsumrev2  14302  fsumparts  14325  fsumiun  14340  isumnn0nn  14359  harmonic  14376  0.999...OLD  14398  fprod2d  14496  bpoly2  14573  bpoly3  14574  bpoly4  14575  ege2le3  14605  cos1bnd  14702  efieq1re  14714  eirrlem  14717  qnnen  14727  cpnnen  14743  ruclem6  14749  3dvds  14836  3dvdsOLD  14837  pwp1fsum  14898  m1bits  14946  algrp1  15071  phiprmpw  15265  prmreclem4  15407  4sqlem11  15443  4sqlem19  15451  dec5dvds  15552  decsplit1  15570  decsplit1OLD  15574  5prm  15599  7prm  15601  1259lem2  15623  1259lem3  15624  1259lem4  15625  1259lem5  15626  1259prm  15627  2503lem1  15628  2503lem2  15629  2503lem3  15630  2503prm  15631  4001lem1  15632  4001lem2  15633  4001lem3  15634  4001lem4  15635  4001prm  15636  ndxid  15662  strle1  15746  grpbasex  15765  grpplusgx  15766  quslem  15972  xpslem  16002  acsfn1  16091  acsfn2  16093  comfffval2  16130  xpchomfval  16588  xpccofval  16591  1stfval  16600  2ndfval  16603  oduleg  16901  ismgmid  17033  grpinvfvi  17232  gaorb  17509  cntri  17532  cntrsubgnsg  17542  cntrnsg  17543  oppglem  17549  oppgcntr  17564  gsumwrev  17565  symgbas  17569  symgga  17595  cayleylem1  17601  psgnunilem2  17684  efgval2  17906  efgredlemc  17927  efgcpbllema  17936  frgpnabllem1  18045  gsumzaddlem  18090  mgplem  18263  opprlem  18397  oppr0  18402  opprneg  18404  rlmscaf  18975  mplbas  19196  mpladd  19209  mplmul  19210  mplvsca2  19213  ressmplbas2  19222  ltbwe  19239  evlslem4  19275  psr1bas2  19327  ply1bas  19332  ply1assa  19336  mplplusg  19357  mplmulr  19358  psr1plusg  19359  psr1vsca  19360  psr1mulr  19361  ply1plusg  19362  ply1vsca  19363  ply1mulr  19364  ply1mpl0  19392  ply1mpl1  19394  coe1mul  19407  xrsds  19554  gsumfsum  19578  zringunit  19603  cnmsgngrp  19689  psgnfix2  19709  relt  19725  ocv0  19782  thlle  19802  thlleval  19803  dsmmval2  19841  frlmip  19878  matgsum  20004  smadiadetglem1  20238  indistpsx  20566  iuncld  20601  tgrest  20715  resstopn  20742  leordtval2  20768  xkouni  21154  ptclsg  21170  ptuncnv  21362  ptunhmeo  21363  alexsubALTlem4  21606  tsmsf1o  21700  ucnimalem  21836  ressxms  22081  uniretop  22308  cnfldtopn  22327  xrtgioo  22349  zcld  22356  icccmp  22368  xrge0gsumle  22376  xrge0tsms  22377  metnrmlem3  22403  fsum2cn  22413  cnmpt2pc  22466  oprpiece1res1  22489  oprpiece1res2  22490  evth  22497  evth2  22498  om1opn  22575  pi1xfrf  22592  pi1xfrcnv  22596  pi1cof  22598  clsocv  22775  cncmet  22844  cnflduss  22877  rrxprds  22902  ehlbase  22919  ismbl  23018  shftmbl  23030  ioorinv  23067  itg1addlem4  23189  itg2cnlem1  23251  iblitg  23258  itg0  23269  itgss3  23304  ditgneg  23344  limcdif  23363  limciun  23381  dvexp  23439  dvef  23464  dvcnvrelem2  23502  ftc1  23526  plyremlem  23780  aannenlem2  23805  taylply2  23843  dvradcnv  23896  pserdvlem2  23903  reefgim  23925  cospi  23945  sincos6thpi  23988  tanregt0  24006  dflog2  24028  logfac  24068  dvlog  24114  cxpexp  24131  cxpmul2  24152  cxpsqrt  24166  dvsqrt  24200  dvcnsqrt  24202  cxpcn2  24204  ang180lem2  24257  isosctrlem2  24266  1cubrlem  24285  1cubr  24286  quart1lem  24299  atancj  24354  atanlogaddlem  24357  atansopn  24376  leibpilem2  24385  log2cnv  24388  log2ublem3  24392  birthdaylem1  24395  birthdaylem2  24396  birthday  24398  dfarea  24404  lgamgulmlem5  24476  lgambdd  24480  wilthlem2  24512  ftalem3  24518  ftalem7  24522  basellem2  24525  ppiprm  24594  ppinprm  24595  chtprm  24596  chtnprm  24597  ppi2  24613  ppi3  24614  ppiub  24646  chtub  24654  bclbnd  24722  bposlem8  24733  lgsdilem  24766  lgsdir2lem1  24767  lgsdir2lem2  24768  lgsdir2lem3  24769  lgsquadlem2  24823  lgsquad2lem2  24827  2lgsoddprmlem3c  24854  rplogsum  24933  mulog2sumlem2  24941  pnt2  25019  istrkg2ld  25076  axsegconlem9  25523  ax5seglem7  25533  usgrares1  25705  cusgrares  25767  wwlknprop  25980  wwlknfi  26032  wlknwwlknvbij  26034  clwwlkvbij  26095  eupath2lem3  26272  ex-pw  26444  ex-xp  26451  ex-rn  26455  nvvop  26632  nvm  26666  cnims  26733  ip0i  26870  ip1ilem  26871  ipdirilem  26874  ipasslem10  26884  h2hva  27021  h2hsm  27022  h2hvs  27024  axhfvadd-zf  27029  axhvcom-zf  27030  axhvass-zf  27031  axhv0cl-zf  27032  axhvaddid-zf  27033  axhfvmul-zf  27034  axhvmulid-zf  27035  axhvmulass-zf  27036  axhvdistr1-zf  27037  axhvdistr2-zf  27038  axhvmul0-zf  27039  axhfi-zf  27040  axhis1-zf  27041  axhis2-zf  27042  axhis3-zf  27043  axhis4-zf  27044  axhcompl-zf  27045  normlem0  27156  normlem1  27157  normlem2  27158  normlem4  27160  normlem9  27165  bcseqi  27167  dfhnorm2  27169  norm3difi  27194  normpari  27201  normpar2i  27203  polid2i  27204  polidi  27205  hhba  27214  hhims  27219  hhims2  27220  hhsssh  27316  hhssims  27322  hhssims2  27323  shsval3i  27437  dfch2  27456  cmcm2i  27642  fh2  27668  qlaxr3i  27685  spansnji  27695  pjcji  27733  ho0val  27799  df0op2  27801  hosd1i  27871  hosd2i  27872  eigorthi  27886  hhlnoi  27949  hhnmoi  27950  hhbloi  27951  bra0  27999  nmop0  28035  nmfn0  28036  lnopeq0lem1  28054  lnopunilem1  28059  lnophmlem2  28066  nmopcoadji  28150  pjhmopidm  28232  cvmdi  28373  cdj3lem3  28487  cdj3lem3b  28489  abrexdomjm  28535  uniin1  28556  uniin2  28557  iundifdifd  28568  iundifdif  28569  mpt2mptxf  28666  df1stres  28670  df2ndres  28671  fcobijfs  28695  resf1o  28699  fpwrelmapffslem  28701  xrslt  28813  xrsclat  28817  gsumle  28916  xrge0tsmsd  28922  xrge0slmod  28981  fimaproj  29034  circtopn  29038  tpr2rico  29092  xrge0mulc1cn  29121  lmxrge0  29132  esumpfinvallem  29269  esumcocn  29275  hasheuni  29280  esumcvg  29281  rossros  29376  measinblem  29416  aean  29440  sxbrsigalem3  29467  dya2iocival  29468  dya2iocucvr  29479  sxbrsigalem1  29480  sxbrsigalem2  29481  sxbrsigalem5  29483  sxbrsiga  29485  fiunelcarsg  29511  eulerpartlem1  29562  eulerpartgbij  29567  fibp1  29596  coinfliplem  29673  coinflipprob  29674  ballotlemfval  29684  ballotth  29732  sgnneg  29735  plymulx  29757  bnj1400  29966  bnj66  29990  bnj882  30056  derang0  30211  subfacp1lem1  30221  subfacp1lem6  30227  kur14lem7  30254  cvmsss2  30316  cvmliftlem8  30334  cvmliftlem10  30336  msubfval  30481  quad3  30624  bcprod  30683  bccolsum  30684  faclim  30691  dftrpred2  30769  bdayfo  30880  pprodcnveq  30966  dfon4  30976  fobigcup  30983  dfiota3  31006  dfrecs2  31033  dfrdg4  31034  dfint3  31035  rankeq1o  31254  refssfne  31329  ssoninhaus  31423  onint1  31424  bj-rababwv  31857  bj-inrab3  31913  rnmptsn  32154  dissneq  32160  dffinxpf  32194  finxpreclem4  32203  rabiun  32348  ptrest  32374  poimirlem3  32378  poimirlem4  32379  poimirlem13  32388  poimirlem16  32391  poimirlem22  32397  poimirlem26  32401  poimirlem27  32402  poimirlem30  32405  cnambfre  32424  ftc1anclem8  32458  fnopabco  32483  abrexdom  32491  cncfres  32530  scottexf  32942  scott0f  32943  cdleme3d  34332  cdleme7a  34344  cdleme31sdnN  34489  cdlemk45  35049  mapfzcons  36093  eldioph4b  36189  diophren  36191  pwssplit4  36473  pwfi2f1o  36480  frlmpwfi  36482  mendplusgfval  36570  mendmulrfval  36572  mendvscafval  36575  idomodle  36589  cytpval  36602  arearect  36616  relintab  36704  dfid7  36734  cnvrcl0  36747  dfrtrcl5  36751  dfrcl3  36782  dfrcl4  36783  comptiunov2i  36813  corcltrcl  36846  neicvgnvo  37229  inductionexd  37269  nznngen  37333  hashnzfz2  37338  lhe4.4ex1a  37346  dvradcnv2  37364  binomcxplemrat  37367  binomcxplemnotnn0  37373  compne  37461  refsum2cnlem1  38015  fiiuncl  38055  rnmptc  38144  iccdifprioo  38386  lptre2pt  38504  limclner  38515  stoweidlem13  38703  stoweidlem32  38722  stoweidlem62  38752  wallispi2lem2  38762  stirlinglem14  38777  dirkertrigeqlem1  38788  dirkercncflem4  38796  fourierdlem42  38839  fourierdlem73  38869  fourierdlem81  38877  fourierdlem92  38888  fourierdlem103  38899  fourierdlem104  38900  fouriercnp  38916  fouriersw  38921  sge0tsms  39070  sge0iunmptlemfi  39103  ovolval5lem3  39341  cnfsmf  39424  m11nprm  39854  opoeALTV  39930  evengpop3  40012  rnfdmpr  40134  nbgrnvtx0  40558  rusgrprc  40785  wwlksnfi  41107  wlksnwwlknvbij  41109  clwwlksvbij  41224  konigsbergumgr  41415  konigsbergupgrOLD  41416  cznabel  41741  cznrng  41742  mpt2mptx2  41901  amgmlemALT  42314
  Copyright terms: Public domain W3C validator