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

Theorem eqtr4i 2676
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 2660 . 2 𝐵 = 𝐶
41, 3eqtri 2673 1 𝐴 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  3eqtr2i  2679  3eqtr2ri  2680  3eqtr4i  2683  3eqtr4ri  2684  rabab  3254  cbvralcsf  3598  cbvrabcsf  3601  dfin5  3615  dfdif2  3616  uneqin  3911  unrab  3931  inrab  3932  inrab2  3933  difrab  3934  dfrab3ss  3938  rabun2  3939  difidALT  3982  rabxm  3994  elnelun  3997  elnelunOLD  3999  difdifdir  4089  dfif3  4133  dfif5  4135  rabsnif  4290  tpidm  4325  ssunpr  4397  sstp  4399  opidg  4452  dfint2  4509  iunrab  4599  uniiun  4605  intiin  4606  0iin  4610  mptv  4784  dfepfr  5128  epfrc  5129  xpundi  5205  xpundir  5206  csbcnv  5338  resiun2  5453  resopab  5481  opabresid  5490  dffr3  5533  dfse2  5534  cnvun  5573  imaundir  5581  imainrect  5610  cnvcnv2  5623  cnvcnvres  5633  dmtpop  5647  rnsnopg  5650  rnco2  5680  dmco  5681  co01  5688  unidmrn  5703  dfdm2  5705  predidm  5740  tz6.26  5749  dfmpt3  6052  mptun  6063  funcocnv2  6199  dffv2  6310  fnasrn  6451  fpr  6461  fmptap  6477  riotav  6656  dmoprab  6783  rnoprab2  6786  mpt2v  6792  mpt2mptx  6793  abrexex2g  7186  abrexex2OLD  7192  1stval2  7227  2ndval2  7228  fo1st  7230  fo2nd  7231  xp2  7247  dfoprab4f  7270  offval22  7298  fmpt2co  7305  tposmpt2  7434  tposconst  7435  recsfval  7522  rdgsucmpt2  7571  frsucmpt2  7580  df2o3  7618  o1p1e2  7665  o2p2e4  7666  oarec  7687  omopthlem2  7781  ecqs  7854  qliftf  7878  erovlem  7886  mapsnf1o3  7948  ixp0x  7978  omf1o  8104  xpf1o  8163  mapunen  8170  enp1ilem  8235  pwfi  8302  marypha1lem  8380  marypha2lem4  8385  dfoi  8457  infeq5i  8571  oemapso  8617  cantnflem1  8624  rankelop  8775  leweon  8872  r0weon  8873  kmlem11  9020  infcda1  9053  ackbij1lem16  9095  cf0  9111  cfsmolem  9130  alephsuc3  9440  fpwwe  9506  canthp1lem1  9512  wuncval2  9607  prlem936  9907  m1p1sr  9951  m1m1sr  9952  dfcnqs  10001  ssxr  10145  mul02lem2  10251  addid1  10254  2p2e4  11182  3p2e5  11198  3p3e6  11199  4p2e6  11200  4p3e7  11201  4p4e8  11202  5p2e7  11203  5p3e8  11204  5p4e9  11205  5p5e10OLD  11206  6p2e8  11207  6p3e9  11208  6p4e10OLD  11209  7p2e9  11210  7p3e10OLD  11211  8p2e10OLD  11212  nnzrab  11443  nn0zrab  11444  dec0u  11558  dec0uOLD  11559  dec0h  11560  dec0hOLD  11561  decsuc  11573  decsucOLD  11574  decsucc  11588  decsuccOLD  11589  numma  11595  decma  11602  decmaOLD  11603  decmac  11604  decmacOLD  11605  decma2c  11606  decma2cOLD  11607  decadd  11608  decaddOLD  11609  decaddc  11610  decaddcOLD  11611  decmul1  11623  decmul1OLD  11624  decmul1c  11625  decmul1cOLD  11626  decmul2c  11627  decmul2cOLD  11628  5p5e10  11634  6p4e10  11636  7p3e10  11641  8p2e10  11648  5t5e25  11677  5t5e25OLD  11678  6t6e36  11684  6t6e36OLD  11685  8t6e48  11697  8t6e48OLD  11698  nn0uz  11760  nnuz  11761  xaddcom  12109  x2times  12167  ioomax  12286  iccmax  12287  ioopos  12288  ioorp  12289  prunioo  12339  fseq1p1m1  12452  fzo13pr  12592  fzo0to2pr  12593  fzo0to3tp  12594  om2uzrdg  12795  fzennn  12807  irec  13004  sq10e99m1  13089  sq10e99m1OLD  13092  facnn  13102  fac0  13103  faclbnd2  13118  faclbnd4lem1  13120  hashfun  13262  hashbclem  13274  hashf1lem1  13277  hashf1lem2  13278  fz1isolem  13283  swrdccatin1  13529  swrdccat3blem  13541  s1co  13625  s2eq2s1eq  13727  s3eqs2s1eq  13729  ofs2  13756  dfid5  13811  dfid6  13812  fsumrev2  14558  fsumparts  14582  fsumiun  14597  isumnn0nn  14618  harmonic  14635  0.999...OLD  14657  fprod2d  14755  bpoly2  14832  bpoly3  14833  bpoly4  14834  ege2le3  14864  cos1bnd  14961  efieq1re  14973  eirrlem  14976  qnnen  14986  cpnnen  15002  ruclem6  15008  3dvds  15099  3dvdsOLD  15100  pwp1fsum  15161  m1bits  15209  algrp1  15334  phiprmpw  15528  prmreclem4  15670  4sqlem11  15706  4sqlem19  15714  dec5dvds  15815  decsplit1  15833  decsplit1OLD  15837  5prm  15862  7prm  15864  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  ndxidOLD  15931  strle1  16020  grpbasex  16041  grpplusgx  16042  quslem  16250  xpslem  16280  acsfn1  16369  acsfn2  16371  comfffval2  16408  xpchomfval  16866  xpccofval  16869  1stfval  16878  2ndfval  16881  oduleg  17179  ismgmid  17311  grpinvfvi  17510  gaorb  17786  cntri  17809  cntrsubgnsg  17819  cntrnsg  17820  oppglem  17826  oppgcntr  17841  gsumwrev  17842  symgbas  17846  symgga  17872  cayleylem1  17878  psgnunilem2  17961  efgval2  18183  efgredlemc  18204  efgcpbllema  18213  frgpnabllem1  18322  gsumzaddlem  18367  mgplem  18540  opprlem  18674  oppr0  18679  opprneg  18681  rmodislmod  18979  rlmscaf  19256  mplbas  19477  mpladd  19490  mplmul  19491  mplvsca2  19494  ressmplbas2  19503  ltbwe  19520  evlslem4  19556  psr1bas2  19608  ply1bas  19613  ply1assa  19617  mplplusg  19638  mplmulr  19639  psr1plusg  19640  psr1vsca  19641  psr1mulr  19642  ply1plusg  19643  ply1vsca  19644  ply1mulr  19645  ply1mpl0  19673  ply1mpl1  19675  coe1mul  19688  xrsds  19837  gsumfsum  19861  zringunit  19884  cnmsgngrp  19973  psgnfix2  19993  relt  20009  ocv0  20069  thlle  20089  thlleval  20090  dsmmval2  20128  frlmip  20165  matgsum  20291  smadiadetglem1  20525  indistpsx  20862  iuncld  20897  tgrest  21011  resstopn  21038  leordtval2  21064  xkouni  21450  ptclsg  21466  ptuncnv  21658  ptunhmeo  21659  alexsubALTlem4  21901  tsmsf1o  21995  ucnimalem  22131  ressxms  22377  uniretop  22613  cnfldtopn  22632  xrtgioo  22656  zcld  22663  icccmp  22675  xrge0gsumle  22683  xrge0tsms  22684  metnrmlem3  22711  fsum2cn  22721  cnmpt2pc  22774  oprpiece1res1  22797  oprpiece1res2  22798  evth  22805  evth2  22806  om1opn  22882  pi1xfrf  22899  pi1xfrcnv  22903  pi1cof  22905  clsocv  23095  cncmet  23165  cnflduss  23198  rrxprds  23223  ehlbase  23240  ismbl  23340  shftmbl  23352  ioorinv  23390  itg1addlem4  23511  itg2cnlem1  23573  iblitg  23580  itg0  23591  itgss3  23626  ditgneg  23666  limcdif  23685  limciun  23703  dvexp  23761  dvef  23788  dvcnvrelem2  23826  ftc1  23850  plyremlem  24104  aannenlem2  24129  taylply2  24167  dvradcnv  24220  pserdvlem2  24227  reefgim  24249  cospi  24269  sincos6thpi  24312  tanregt0  24330  dflog2  24352  logfac  24392  dvlog  24442  cxpexp  24459  cxpmul2  24480  cxpsqrt  24494  dvsqrt  24528  dvcnsqrt  24530  cxpcn2  24532  ang180lem2  24585  isosctrlem2  24594  1cubrlem  24613  1cubr  24614  quart1lem  24627  atancj  24682  atanlogaddlem  24685  atansopn  24704  leibpilem2  24713  log2cnv  24716  log2ublem3  24720  birthdaylem1  24723  birthdaylem2  24724  birthday  24726  dfarea  24732  lgamgulmlem5  24804  lgambdd  24808  wilthlem2  24840  ftalem3  24846  ftalem7  24850  basellem2  24853  ppiprm  24922  ppinprm  24923  chtprm  24924  chtnprm  24925  ppi2  24941  ppi3  24942  ppiub  24974  chtub  24982  bclbnd  25050  bposlem8  25061  lgsdilem  25094  lgsdir2lem1  25095  lgsdir2lem2  25096  lgsdir2lem3  25097  lgsquadlem2  25151  lgsquad2lem2  25155  2lgsoddprmlem3c  25182  rplogsum  25261  mulog2sumlem2  25269  pnt2  25347  istrkg2ld  25404  axsegconlem9  25850  ax5seglem7  25860  iedgedg  25988  uspgrf1oedg  26113  nbgrcl  26272  nbgrnvtx0  26277  rusgrprc  26542  wlkiswwlks2lem4  26826  wlkiswwlks2lem5  26827  wwlksnfi  26869  wlksnwwlknvbij  26871  clwwlkvbij  27088  clwwlkvbijOLD  27089  konigsbergumgr  27229  ex-pw  27416  ex-xp  27423  ex-rn  27427  nvvop  27592  nvm  27624  cnims  27676  ip0i  27808  ip1ilem  27809  ipdirilem  27812  ipasslem10  27822  h2hva  27959  h2hsm  27960  h2hvs  27962  axhfvadd-zf  27967  axhvcom-zf  27968  axhvass-zf  27969  axhv0cl-zf  27970  axhvaddid-zf  27971  axhfvmul-zf  27972  axhvmulid-zf  27973  axhvmulass-zf  27974  axhvdistr1-zf  27975  axhvdistr2-zf  27976  axhvmul0-zf  27977  axhfi-zf  27978  axhis1-zf  27979  axhis2-zf  27980  axhis3-zf  27981  axhis4-zf  27982  axhcompl-zf  27983  normlem0  28094  normlem1  28095  normlem2  28096  normlem4  28098  normlem9  28103  bcseqi  28105  dfhnorm2  28107  norm3difi  28132  normpari  28139  normpar2i  28141  polid2i  28142  polidi  28143  hhba  28152  hhims  28157  hhims2  28158  hhsssh  28254  hhssims  28260  hhssims2  28261  shsval3i  28375  dfch2  28394  cmcm2i  28580  fh2  28606  qlaxr3i  28623  spansnji  28633  pjcji  28671  ho0val  28737  df0op2  28739  hosd1i  28809  hosd2i  28810  eigorthi  28824  hhlnoi  28887  hhnmoi  28888  hhbloi  28889  bra0  28937  nmop0  28973  nmfn0  28974  lnopeq0lem1  28992  lnopunilem1  28997  lnophmlem2  29004  nmopcoadji  29088  pjhmopidm  29170  cvmdi  29311  cdj3lem3  29425  cdj3lem3b  29427  abrexdomjm  29471  uniin1  29493  uniin2  29494  iundifdifd  29506  iundifdif  29507  mpt2mptxf  29605  df1stres  29609  df2ndres  29610  fcobijfs  29629  resf1o  29633  fpwrelmapffslem  29635  dpval3  29730  dp3mul10  29734  dpadd2  29746  dpmul4  29750  xrslt  29804  xrsclat  29808  gsumle  29907  xrge0tsmsd  29913  xrge0slmod  29972  fimaproj  30028  circtopn  30032  tpr2rico  30086  xrge0mulc1cn  30115  lmxrge0  30126  esumpfinvallem  30264  esumcocn  30270  hasheuni  30275  esumcvg  30276  rossros  30371  measinblem  30411  aean  30435  sxbrsigalem3  30462  dya2iocival  30463  dya2iocucvr  30474  sxbrsigalem1  30475  sxbrsigalem2  30476  sxbrsigalem5  30478  sxbrsiga  30480  fiunelcarsg  30506  eulerpartlem1  30557  eulerpartgbij  30562  fibp1  30591  coinfliplem  30668  coinflipprob  30669  ballotlemfval  30679  ballotth  30727  sgnneg  30730  plymulx  30753  circlemethhgt  30849  hgt750lem2  30858  bnj1400  31032  bnj66  31056  bnj882  31122  derang0  31277  subfacp1lem1  31287  subfacp1lem6  31293  kur14lem7  31320  cvmsss2  31382  cvmliftlem8  31400  cvmliftlem10  31402  msubfval  31547  quad3  31690  bcprod  31750  bccolsum  31751  faclim  31758  dftrpred2  31843  frrlem6  31914  frrlem11  31917  bdayfo  31953  pprodcnveq  32115  dfon4  32125  fobigcup  32132  dfiota3  32155  dfrecs2  32182  dfrdg4  32183  dfint3  32184  rankeq1o  32403  refssfne  32478  ssoninhaus  32572  onint1  32573  bj-rababwv  32992  bj-inrab3  33050  rnmptsn  33312  dissneq  33318  dffinxpf  33352  finxpreclem4  33361  rabiun  33512  ptrest  33538  poimirlem3  33542  poimirlem4  33543  poimirlem13  33552  poimirlem16  33555  poimirlem22  33561  poimirlem26  33565  poimirlem27  33566  poimirlem30  33569  cnambfre  33588  ftc1anclem8  33622  fnopabco  33647  abrexdom  33655  cncfres  33694  scottexf  34106  scott0f  34107  inres2  34150  dfres4  34202  xrnres  34300  xrnres2  34301  dfcoss2  34311  dfcoss4  34313  1cossres  34324  dmcoss2  34344  1cosscnvxrn  34365  cdleme3d  35836  cdleme7a  35848  cdleme31sdnN  35992  cdlemk45  36552  mapfzcons  37596  eldioph4b  37692  diophren  37694  pwssplit4  37976  pwfi2f1o  37983  frlmpwfi  37985  mendplusgfval  38072  mendmulrfval  38074  mendvscafval  38077  idomodle  38091  cytpval  38104  arearect  38118  relintab  38206  dfid7  38236  cnvrcl0  38249  dfrtrcl5  38253  dfrcl3  38284  dfrcl4  38285  comptiunov2i  38315  corcltrcl  38348  neicvgnvo  38730  inductionexd  38770  nznngen  38832  hashnzfz2  38837  lhe4.4ex1a  38845  dvradcnv2  38863  binomcxplemrat  38866  binomcxplemnotnn0  38872  compneOLD  38961  refsum2cnlem1  39510  fiiuncl  39548  rnmptc  39667  iccdifprioo  40060  lptre2pt  40190  limclner  40201  stoweidlem13  40548  stoweidlem32  40567  stoweidlem62  40597  wallispi2lem2  40607  stirlinglem14  40622  dirkertrigeqlem1  40633  dirkercncflem4  40641  fourierdlem42  40684  fourierdlem73  40714  fourierdlem81  40722  fourierdlem92  40733  fourierdlem103  40744  fourierdlem104  40745  fouriercnp  40761  fouriersw  40766  sge0tsms  40915  sge0iunmptlemfi  40948  ovolval5lem3  41189  cnfsmf  41270  rnfdmpr  41623  fvmptrabdm  41632  m11nprm  41843  opoeALTV  41919  sbgoldbo  42000  evengpop3  42011  cznabel  42279  cznrng  42280  mpt2mptx2  42438  amgmlemALT  42877
  Copyright terms: Public domain W3C validator