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

Theorem eqtr4i 2769
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 2747 . 2 𝐵 = 𝐶
41, 3eqtri 2766 1 𝐴 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2730
This theorem is referenced by:  3eqtr2i  2772  3eqtr2ri  2773  3eqtr4i  2776  3eqtr4ri  2777  rabab  3443  cbvralcsf  3865  cbvrabcsf  3868  dfin5  3883  dfdif2  3884  uneqin  4202  notabw  4227  unrab  4229  inrab  4230  inrab2  4231  difrab  4232  dfrab3ss  4236  rabun2  4237  dfnul2  4249  difid  4294  rabxm  4310  elnelun  4313  abf  4326  difdifdir  4412  dfif3  4462  dfif5  4464  rabsnif  4648  tpidm  4683  ssunpr  4754  sstp  4756  opidg  4812  dfint2  4870  iunrab  4970  uniiun  4976  intiin  4977  0iin  4981  mptv  5169  dfepfr  5545  epfrc  5546  xpundi  5626  xpundir  5627  csbcnv  5761  resiun2  5881  resopab  5911  mptresid  5927  opabresidOLD  5928  dffr3  5976  dfse2  5977  cnvun  6015  imaundir  6023  imainrect  6053  cnvcnv2  6065  cnvrescnv  6067  cnvcnvres  6077  dmtpop  6090  rnsnopg  6093  resdifdi  6108  rnco2  6126  dmco  6127  co01  6134  unidmrn  6151  dfdm2  6153  predidm  6193  tz6.26  6210  dfmpt3  6521  mptun  6533  funcocnv2  6694  dffv2  6815  fnasrn  6969  fpr  6978  fmptap  6994  rnmptc  7031  rnmptcOLD  7032  riotav  7184  dmoprab  7321  rnoprab2  7324  mpov  7331  mpomptx  7332  abrexex2g  7746  1stval2  7787  2ndval2  7788  fo1st  7790  fo2nd  7791  xp2  7807  dfoprab4f  7835  offval22  7865  fmpoco  7872  fimaproj  7911  tposmpo  8014  tposconst  8015  recsfval  8126  rdgsucmpt2  8175  frsucmpt2w  8184  frsucmpt2  8185  df2o3  8226  o1p1e2  8276  o2p2e4  8277  o2p2e4OLD  8278  oarec  8299  omopthlem2  8394  ecqs  8472  qliftf  8496  erovlem  8504  fset0  8544  mapsnf1o3  8585  ixp0x  8616  omf1o  8759  xpf1o  8819  mapunen  8826  enp1ilem  8921  pwfiOLD  8984  marypha1lem  9062  marypha2lem4  9067  dfoi  9140  infeq5i  9264  oemapso  9310  cantnflem1  9317  dftrpred2  9337  rankelop  9503  leweon  9638  r0weon  9639  kmlem11  9787  dju1dif  9799  ackbij1lem16  9862  cf0  9878  cfsmolem  9897  alephsuc3  10207  fpwwe  10273  canthp1lem1  10279  wuncval2  10374  prlem936  10674  m1p1sr  10719  m1m1sr  10720  dfcnqs  10769  ssxr  10915  mul02lem2  11022  addid1  11025  2p2e4  11978  3p2e5  11994  3p3e6  11995  4p2e6  11996  4p3e7  11997  4p4e8  11998  5p2e7  11999  5p3e8  12000  5p4e9  12001  6p2e8  12002  6p3e9  12003  7p2e9  12004  nnzrab  12218  nn0zrab  12219  dec0u  12327  dec0h  12328  decsuc  12337  decsucc  12347  numma  12350  decma  12357  decmac  12358  decma2c  12359  decadd  12360  decaddc  12361  decmul1c  12371  decmul2c  12372  5p5e10  12377  6p4e10  12378  7p3e10  12381  8p2e10  12386  5t5e25  12409  6t6e36  12414  8t6e48  12425  nn0uz  12489  nnuz  12490  xaddcom  12843  x2times  12902  ioomax  13023  iccmax  13024  ioopos  13025  ioorp  13026  prunioo  13082  fseq1p1m1  13199  fzo13pr  13339  fzo0to2pr  13340  fzo0to3tp  13341  om2uzrdg  13542  fzennn  13554  irec  13783  sq10e99m1  13844  facnn  13854  fac0  13855  faclbnd2  13870  faclbnd4lem1  13872  hashfun  14017  hashbclem  14029  hashf1lem1  14033  hashf1lem1OLD  14034  hashf1lem2  14035  fz1isolem  14040  swrdccatin1  14303  swrdccat3blem  14317  s1co  14411  s2eq2s1eq  14514  s3eqs2s1eq  14516  ofs2  14547  dfid5  14603  dfid6  14604  fsumrev2  15359  fsumparts  15383  fsumiun  15398  isumnn0nn  15419  harmonic  15436  fprod2d  15556  bpoly2  15632  bpoly3  15633  bpoly4  15634  ege2le3  15664  cos1bnd  15761  efieq1re  15773  eirrlem  15778  qnnen  15787  cpnnen  15803  ruclem6  15809  3dvds  15905  pwp1fsum  15965  m1bits  16012  algrp1  16144  phiprmpw  16342  prmreclem4  16485  4sqlem11  16521  4sqlem19  16529  dec5dvds  16630  decsplit1  16648  5prm  16675  7prm  16677  1259lem2  16698  1259lem3  16699  1259lem4  16700  1259lem5  16701  1259prm  16702  2503lem1  16703  2503lem2  16704  2503lem3  16705  2503prm  16706  4001lem1  16707  4001lem2  16708  4001lem3  16709  4001lem4  16710  4001prm  16711  strle1  16724  grpbasex  16848  grpplusgx  16849  quslem  17061  xpsrnbas  17089  acsfn1  17177  acsfn2  17179  comfffval2  17217  dfinito2  17522  dftermo2  17523  xpchomfval  17699  xpccofval  17702  1stfval  17711  2ndfval  17714  oduleg  17811  ismgmid  18150  efmndbas  18311  smndex2dnrinv  18355  grpinvfvi  18423  gaorb  18714  cntri  18738  cntrsubgnsg  18748  cntrnsg  18749  oppglem  18755  oppgcntr  18770  gsumwrev  18771  symgressbas  18787  symgplusg  18788  symgvalstruct  18802  symgga  18812  cayleylem1  18817  psgnunilem2  18900  efgval2  19127  efgredlemc  19148  efgcpbllema  19157  frgpnabllem1  19271  gsumzaddlem  19319  mgplem  19522  opprlem  19659  oppr0  19664  opprneg  19666  rmodislmod  19980  rlmscaf  20259  xrsds  20419  gsumfsum  20443  zringunit  20466  cnmsgngrp  20554  psgnfix2  20574  relt  20590  ocv0  20652  thlle  20672  thlleval  20673  dsmmval2  20711  frlmip  20753  mplbas  20967  mpladd  20982  mplmul  20984  mplvsca2  20987  ressmplbas2  20997  ltbwe  21014  evlslem4  21047  psr1bas2  21124  ply1bas  21129  ply1assa  21133  mplplusg  21154  mplmulr  21155  psr1plusg  21156  psr1vsca  21157  psr1mulr  21158  ply1plusg  21159  ply1vsca  21160  ply1mulr  21161  ply1mpl0  21189  ply1mpl1  21191  coe1mul  21204  matgsum  21347  smadiadetglem1  21581  indistpsx  21920  iuncld  21955  tgrest  22069  resstopn  22096  leordtval2  22122  xkouni  22509  ptclsg  22525  ptuncnv  22717  ptunhmeo  22718  alexsubALTlem4  22960  tsmsf1o  23055  ucnimalem  23190  ressxms  23436  uniretop  23673  cnfldtopn  23692  xrtgioo  23716  zcld  23723  icccmp  23735  xrge0gsumle  23743  xrge0tsms  23744  metnrmlem3  23771  fsum2cn  23781  cnmpopc  23838  oprpiece1res1  23861  oprpiece1res2  23862  evth  23869  evth2  23870  om1opn  23946  pi1xfrf  23963  pi1xfrcnv  23967  pi1cof  23969  clsocv  24160  cncmet  24232  cnflduss  24266  rrxprds  24299  ehlbase  24325  ismbl  24436  shftmbl  24448  ioorinv  24486  itg1addlem4  24609  itg1addlem4OLD  24610  itg2cnlem1  24672  itg0  24690  itgss3  24725  ditgneg  24767  limcdif  24786  limciun  24804  dvexp  24863  dvef  24890  dvcnvrelem2  24928  ftc1  24952  aannenlem2  25235  dvradcnv  25326  pserdvlem2  25333  reefgim  25355  cospi  25375  sincos6thpi  25418  tanregt0  25441  dflog2  25462  logfac  25502  dvlog  25552  cxpexp  25569  cxpmul2  25590  cxpsqrt  25604  dvsqrt  25641  dvcnsqrt  25643  cxpcn2  25645  isosctrlem2  25715  1cubrlem  25737  1cubr  25738  quart1lem  25751  atancj  25806  atanlogaddlem  25809  atansopn  25828  leibpilem2  25837  log2cnv  25840  log2ublem3  25844  birthdaylem1  25847  birthdaylem2  25848  birthday  25850  dfarea  25856  lgamgulmlem5  25928  lgambdd  25932  ftalem3  25970  basellem2  25977  ppiprm  26046  ppinprm  26047  chtprm  26048  chtnprm  26049  ppi2  26065  ppi3  26066  ppiub  26098  chtub  26106  bclbnd  26174  bposlem8  26185  lgsdilem  26218  lgsdir2lem2  26220  lgsquadlem2  26275  lgsquad2lem2  26279  2lgsoddprmlem3c  26306  rplogsum  26421  mulog2sumlem2  26429  pnt2  26507  istrkg2ld  26564  axsegconlem9  27029  ax5seglem7  27039  iedgedg  27154  uspgrf1oedg  27277  nbgrcl  27436  nbgrnvtx0  27440  rusgrprc  27691  wlkiswwlks2lem4  27969  wlkiswwlks2lem5  27970  clwwlkvbij  28209  konigsbergumgr  28347  ex-pw  28525  ex-xp  28532  ex-rn  28536  nvvop  28703  nvm  28735  cnims  28787  ip0i  28919  ip1ilem  28920  ipdirilem  28923  ipasslem10  28933  h2hva  29068  h2hsm  29069  h2hvs  29071  axhfvadd-zf  29076  axhvcom-zf  29077  axhvass-zf  29078  axhv0cl-zf  29079  axhvaddid-zf  29080  axhfvmul-zf  29081  axhvmulid-zf  29082  axhvmulass-zf  29083  axhvdistr1-zf  29084  axhvdistr2-zf  29085  axhvmul0-zf  29086  axhfi-zf  29087  axhis1-zf  29088  axhis2-zf  29089  axhis3-zf  29090  axhis4-zf  29091  axhcompl-zf  29092  normlem0  29203  normlem1  29204  normlem2  29205  normlem4  29207  normlem9  29212  bcseqi  29214  dfhnorm2  29216  norm3difi  29241  normpari  29248  normpar2i  29250  polid2i  29251  polidi  29252  hhba  29261  hhims  29266  hhims2  29267  hhsssh  29363  hhssims  29368  hhssims2  29369  shsval3i  29482  dfch2  29501  cmcm2i  29687  fh2  29713  qlaxr3i  29730  spansnji  29740  pjcji  29778  ho0val  29844  df0op2  29846  hosd1i  29916  hosd2i  29917  eigorthi  29931  hhlnoi  29994  hhnmoi  29995  hhbloi  29996  bra0  30044  nmop0  30080  nmfn0  30081  lnopeq0lem1  30099  lnopunilem1  30104  lnophmlem2  30111  nmopcoadji  30195  pjhmopidm  30277  cvmdi  30418  cdj3lem3  30532  cdj3lem3b  30534  abrexdomjm  30584  uniin1  30623  uniin2  30624  iundifdifd  30633  iundifdif  30634  mpomptxf  30749  df1stres  30769  df2ndres  30770  intimafv  30776  fcobijfs  30791  resf1o  30798  fpwrelmapffslem  30800  dpval3  30901  dp3mul10  30905  dpadd2  30917  dpmul4  30921  xrslt  31017  xrsclat  31021  xrge0tsmsd  31049  gsumle  31082  cycpmco2lem7  31131  cycpmconjv  31141  cycpmrn  31142  xrge0slmod  31275  lsmsnorb2  31307  rgmoddim  31420  circtopn  31514  tpr2rico  31589  xrge0mulc1cn  31618  lmxrge0  31629  esumpfinvallem  31767  esumcocn  31773  hasheuni  31778  esumcvg  31779  rossros  31873  measinblem  31913  aean  31937  sxbrsigalem3  31964  dya2iocival  31965  dya2iocucvr  31976  sxbrsigalem1  31977  sxbrsigalem2  31978  sxbrsigalem5  31980  sxbrsiga  31982  fiunelcarsg  32008  eulerpartlem1  32059  eulerpartgbij  32064  fibp1  32093  coinfliplem  32170  coinflipprob  32171  ballotlemfval  32181  ballotth  32229  sgnneg  32232  plymulx  32252  circlemethhgt  32348  hgt750lem2  32357  bnj1400  32541  bnj66  32566  bnj882  32632  lfuhgr  32805  derang0  32857  subfacp1lem1  32867  subfacp1lem6  32873  kur14lem7  32900  cvmsss2  32962  cvmliftlem8  32980  cvmliftlem10  32982  satfv1lem  33050  msubfval  33212  quad3  33354  bcprod  33435  bccolsum  33436  faclim  33443  bdayfo  33630  bday0s  33772  bday1s  33775  pprodcnveq  33935  dfon4  33945  fobigcup  33952  dfiota3  33975  dfrecs2  34002  dfrdg4  34003  dfint3  34004  rankeq1o  34223  refssfne  34297  ssoninhaus  34387  onint1  34388  bj-rababw  34816  bj-inrab3  34867  bj-imdiridlem  35104  dissneq  35262  dffinxpf  35306  finxpreclem4  35315  rabiun  35500  ptrest  35526  poimirlem3  35530  poimirlem4  35531  poimirlem13  35540  poimirlem16  35543  poimirlem22  35549  poimirlem26  35553  poimirlem27  35554  poimirlem30  35557  cnambfre  35575  ftc1anclem8  35607  fnopabco  35631  abrexdom  35638  cncfres  35673  scottexf  36076  scott0f  36077  inres2  36134  dfres4  36178  xrnres  36278  xrnres2  36279  dfcoss2  36289  dfcoss4  36291  1cossres  36302  dmcoss2  36322  1cosscnvxrn  36343  dfeqvrels2  36451  dfcoeleqvrels  36484  redundss3  36491  dffunsALTV5  36548  cdleme3d  37995  cdleme7a  38007  cdleme31sdnN  38151  cdlemk45  38711  420gcd8e4  39761  lcmeprodgcdi  39762  60lcm7e420  39765  420lcm8e840  39766  3lexlogpow5ineq1  39809  3lexlogpow2ineq1  39813  3lexlogpow2ineq2  39814  3lexlogpow5ineq5  39815  aks4d1p1  39830  2ap1caineq  39839  sticksstones7  39846  sticksstones12a  39851  sticksstones12  39852  imaopab  39935  dfqs2  39940  dfqs3  39941  decaddcom  40034  nn0expgcd  40058  sn-00idlem2  40105  reixi  40127  mapfzcons  40256  eldioph4b  40351  diophren  40353  pwssplit4  40632  pwfi2f1o  40639  frlmpwfi  40641  mendplusgfval  40728  mendmulrfval  40730  mendvscafval  40733  idomodle  40739  cytpval  40752  arearect  40764  tr3dom  40835  alephiso2  40856  alephiso3  40857  relintab  40882  dfid7  40911  cnvrcl0  40924  dfrtrcl5  40928  dfrcl3  40975  dfrcl4  40976  comptiunov2i  41006  corcltrcl  41039  neicvgnvo  41417  inductionexd  41457  mnuprdlem2  41579  nznngen  41622  hashnzfz2  41627  lhe4.4ex1a  41635  dvradcnv2  41653  binomcxplemrat  41656  binomcxplemnotnn0  41662  refsum2cnlem1  42268  fiiuncl  42301  iccdifprioo  42744  lptre2pt  42871  limclner  42882  stoweidlem13  43244  stoweidlem32  43263  stoweidlem62  43293  wallispi2lem2  43303  stirlinglem14  43318  dirkertrigeqlem1  43329  dirkercncflem4  43337  fourierdlem42  43380  fourierdlem73  43410  fourierdlem81  43418  fourierdlem92  43429  fourierdlem103  43440  fourierdlem104  43441  fouriercnp  43457  fouriersw  43462  sge0tsms  43608  sge0iunmptlemfi  43641  ovolval5lem3  43882  cnfsmf  43963  rnfdmpr  44460  fvmptrabdm  44472  fundcmpsurinjlem1  44538  m11nprm  44741  opoeALTV  44823  nfermltl8rev  44882  sbgoldbo  44927  evengpop3  44938  cznabel  45200  cznrng  45201  mpomptx2  45358  2sphere  45783  itscnhlinecirc02plem3  45818  inlinecirc02p  45821  icccldii  45900  dfnrm2  45913  dfnrm3  45914  amgmlemALT  46193
  Copyright terms: Public domain W3C validator