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

Theorem eqtr4i 2459
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtr4i.1  |-  A  =  B
eqtr4i.2  |-  C  =  B
Assertion
Ref Expression
eqtr4i  |-  A  =  C

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2  |-  A  =  B
2 eqtr4i.2 . . 3  |-  C  =  B
32eqcomi 2440 . 2  |-  B  =  C
41, 3eqtri 2456 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  3eqtr2i  2462  3eqtr2ri  2463  3eqtr4i  2466  3eqtr4ri  2467  rabab  2973  cbvralcsf  3311  cbvrabcsf  3314  dfin5  3328  dfdif2  3329  uneqin  3592  unrab  3612  inrab  3613  inrab2  3614  difrab  3615  dfrab3ss  3619  rabun2  3620  rabxm  3650  difidALT  3697  difdifdir  3715  dfif3  3749  dfif5  3751  tpidm  3908  ssunpr  3961  sstp  3963  dfint2  4052  iunrab  4138  uniiun  4144  intiin  4145  0iin  4149  mptv  4301  dfepfr  4567  epfrc  4568  xpundi  4930  xpundir  4931  resiun2  5166  resopab  5187  opabresid  5194  dffr3  5236  dfse2  5237  cnvun  5277  imaundir  5285  imainrect  5312  cnvcnv2  5324  cnvcnvres  5333  dmtpop  5346  rnsnopg  5349  rnco2  5377  dmco  5378  co01  5384  unidmrn  5399  dfdm2  5401  dfmpt3  5567  mptun  5575  funcocnv2  5700  dffv2  5796  fnasrn  5912  fpr  5914  fmptap  5923  abrexex2g  5988  abrexex2  6001  dmoprab  6154  rnoprab2  6157  mpt2v  6163  mpt2mptx  6164  1stval2  6364  2ndval2  6365  fo1st  6366  fo2nd  6367  xp2  6384  dfoprab4f  6405  fmpt2co  6430  tposmpt2  6516  riotav  6554  cbvriota  6560  recsfval  6642  rdgsucmpt2  6688  frsucmpt2  6697  df2o3  6737  o1p1e2  6784  oarec  6805  omopthlem2  6899  ecqs  6968  qliftf  6992  erovlem  7000  mapsnf1o3  7062  ixp0x  7090  omf1o  7211  xpf1o  7269  mapunen  7276  enp1ilem  7342  pwfi  7402  marypha1lem  7438  marypha2lem4  7443  dfoi  7480  infeq5i  7591  oemapso  7638  cantnflem1  7645  rankelop  7800  leweon  7893  r0weon  7894  kmlem11  8040  infcda1  8073  ackbij1lem16  8115  cf0  8131  cfsmolem  8150  alephsuc3  8455  fpwwe  8521  canthp1lem1  8527  wuncval2  8622  prlem936  8924  m1p1sr  8967  m1m1sr  8968  dfcnqs  9017  ssxr  9145  mul02lem2  9243  addid1  9246  3m1e2  10096  3m1e2OLD  10097  2p2e4  10098  3p2e5  10111  3p3e6  10112  4p2e6  10113  4p3e7  10114  4p4e8  10115  5p2e7  10116  5p3e8  10117  5p4e9  10118  5p5e10  10119  6p2e8  10120  6p3e9  10121  6p4e10  10122  7p2e9  10123  7p3e10  10124  8p2e10  10125  nn0supp  10273  nnzrab  10309  nn0zrab  10310  dec0u  10397  dec0h  10398  decsuc  10405  decsucc  10409  numma  10413  decma  10420  decmac  10421  decma2c  10422  decadd  10423  decaddc  10424  decmul1c  10429  decmul2c  10430  5t5e25  10458  6t6e36  10463  8t6e48  10474  nn0uz  10520  nnuz  10521  xaddcom  10824  x2times  10878  ioomax  10985  iccmax  10986  ioopos  10987  ioorp  10988  prunioo  11025  fseq1p1m1  11122  fzo0to2pr  11184  fzo0to3tp  11185  om2uzrdg  11296  fzennn  11307  irec  11480  binom2aiOLD  11491  facnn  11568  fac0  11569  faclbnd2  11582  faclbnd4lem1  11584  hashfun  11700  hashbclem  11701  hashf1lem1  11704  hashf1lem2  11705  fz1isolem  11710  s1co  11802  fsumrev2  12565  fsumparts  12585  fsumiun  12600  isumnn0nn  12622  harmonic  12638  0.999...  12658  ege2le3  12692  cos1bnd  12788  efieq1re  12800  eirrlem  12803  qnnen  12813  cpnnen  12828  ruclem6  12834  3dvds  12912  m1bits  12952  algrp1  13065  phiprmpw  13165  prmreclem4  13287  4sqlem11  13323  4sqlem19  13331  dec5dvds  13400  decsplit1  13418  5prm  13431  7prm  13433  1259lem2  13451  1259lem3  13452  1259lem4  13453  1259lem5  13454  1259prm  13455  2503lem1  13456  2503lem2  13457  2503lem3  13458  2503prm  13459  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  4001prm  13464  ndxid  13490  strle1  13560  grpbasex  13572  grpplusgx  13573  divslem  13768  xpslem  13798  acsfn1  13886  acsfn2  13888  comfffval2  13927  xpchomfval  14276  xpccofval  14279  1stfval  14288  2ndfval  14291  oduleg  14559  grpinvfvi  14846  gaorb  15084  symgbas  15095  symgga  15109  cayleylem1  15110  cntri  15129  cntrsubgnsg  15139  cntrnsg  15140  oppglem  15146  oppgcntr  15161  gsumwrev  15162  efgval2  15356  efgredlemc  15377  efgcpbllema  15386  frgpnabllem1  15484  gsumzaddlem  15526  mgplem  15653  opprlem  15733  oppr0  15738  opprneg  15740  rlmscaf  16279  mplbas  16493  mpladd  16505  mplmul  16506  mplvsca2  16509  ressmplbas2  16518  ltbwe  16533  evlslem4  16564  psr1bas2  16588  ply1bas  16593  ply1assa  16597  mplplusg  16614  mplmulr  16615  psr1plusg  16616  psr1vsca  16617  psr1mulr  16618  ply1plusg  16619  ply1vsca  16620  ply1mulr  16621  ply1mpl0  16649  ply1mpl1  16650  coe1mul  16663  xrsds  16741  zrngunit  16765  gsumfsum  16766  ocv0  16904  thlle  16924  thlleval  16925  indistpsx  17074  iuncld  17109  tgrest  17223  resstopn  17250  leordtval2  17276  xkouni  17631  ptclsg  17647  ptuncnv  17839  ptunhmeo  17840  alexsubALTlem4  18081  tsmsf1o  18174  ucnimalem  18310  ressxms  18555  uniretop  18796  cnfldtopn  18816  xrtgioo  18837  zcld  18844  icccmp  18856  xrge0gsumle  18864  xrge0tsms  18865  metnrmlem3  18891  fsum2cn  18901  cnmpt2pc  18953  oprpiece1res1  18976  oprpiece1res2  18977  evth  18984  evth2  18985  om1opn  19061  pi1xfrf  19078  pi1xfrcnv  19082  pi1cof  19084  clsocv  19204  cncmet  19275  cnflduss  19310  ismbl  19422  shftmbl  19433  ioorinv  19468  itg1addlem4  19591  itg2cnlem1  19653  iblitg  19660  itg0  19671  itgss3  19706  ditgneg  19744  limcdif  19763  limciun  19781  dvexp  19839  dvef  19864  dvcnvrelem2  19902  ftc1  19926  plyremlem  20221  aannenlem2  20246  taylply2  20284  dvradcnv  20337  pserdvlem2  20344  reefgim  20366  cospi  20380  sincos6thpi  20423  tanregt0  20441  dflog2  20458  logfac  20495  dvlog  20542  cxpexp  20559  cxpmul2  20580  cxpsqr  20594  dvsqr  20628  cxpcn2  20630  ang180lem2  20652  isosctrlem2  20663  1cubrlem  20681  1cubr  20682  quart1lem  20695  atancj  20750  atanlogaddlem  20753  atansopn  20772  leibpilem2  20781  log2cnv  20784  log2ublem3  20788  birthdaylem1  20790  birthdaylem2  20791  birthday  20793  dfarea  20799  wilthlem2  20852  ftalem3  20857  ftalem7  20861  basellem2  20864  ppiprm  20934  ppinprm  20935  chtprm  20936  chtnprm  20937  ppi2  20953  ppi3  20954  ppiub  20988  chtub  20996  bclbnd  21064  bposlem8  21075  lgsdilem  21106  lgsdir2lem1  21107  lgsdir2lem2  21108  lgsdir2lem3  21109  lgsquadlem2  21139  lgsquad2lem2  21143  rplogsum  21221  mulog2sumlem2  21229  pnt2  21307  usgrares1  21424  cusgrares  21481  eupath2lem3  21701  konigsberg  21709  ex-pw  21737  ex-xp  21744  ex-rn  21748  ablosn  21935  efghgrp  21961  nvvop  22088  nvm  22122  cnims  22189  ip0i  22326  ip1ilem  22327  ipdirilem  22330  ipasslem10  22340  h2hva  22477  h2hsm  22478  h2hvs  22480  axhfvadd-zf  22485  axhvcom-zf  22486  axhvass-zf  22487  axhv0cl-zf  22488  axhvaddid-zf  22489  axhfvmul-zf  22490  axhvmulid-zf  22491  axhvmulass-zf  22492  axhvdistr1-zf  22493  axhvdistr2-zf  22494  axhvmul0-zf  22495  axhfi-zf  22496  axhis1-zf  22497  axhis2-zf  22498  axhis3-zf  22499  axhis4-zf  22500  axhcompl-zf  22501  normlem0  22611  normlem1  22612  normlem2  22613  normlem4  22615  normlem9  22620  bcseqi  22622  dfhnorm2  22624  norm3difi  22649  normpari  22656  normpar2i  22658  polid2i  22659  polidi  22660  hhba  22669  hhims  22674  hhims2  22675  hhsssh  22769  hhssims  22775  hhssims2  22776  shsval3i  22890  dfch2  22909  cmcm2i  23095  fh2  23121  qlaxr3i  23138  spansnji  23148  pjcji  23186  ho0val  23253  df0op2  23255  hosd1i  23325  hosd2i  23326  eigorthi  23340  hhlnoi  23403  hhnmoi  23404  hhbloi  23405  bra0  23453  nmop0  23489  nmfn0  23490  lnopeq0lem1  23508  lnopunilem1  23513  lnophmlem2  23520  nmopcoadji  23604  pjhmopidm  23686  cvmdi  23827  cdj3lem3  23941  cdj3lem3b  23943  abrexdomjm  23988  iundifdifd  24012  iundifdif  24013  df1stres  24091  df2ndres  24092  xrslt  24198  xrge0tsmsd  24223  relt  24276  tpr2rico  24310  xrge0mulc1cn  24327  lmxrge0  24337  esumpfinvallem  24464  esumcocn  24470  hasheuni  24475  esumcvg  24476  measinblem  24574  aean  24595  sxbrsigalem3  24622  dya2iocival  24623  dya2iocucvr  24634  sxbrsigalem1  24635  sxbrsigalem2  24636  sxbrsigalem5  24638  sxbrsiga  24640  sitgclbn  24657  coinfliplem  24736  coinflipprob  24737  ballotlemfval  24747  ballotth  24795  lgamgulmlem5  24817  lgambdd  24821  derang0  24855  subfacp1lem1  24865  subfacp1lem6  24871  kur14lem7  24898  cvmsss2  24961  cvmliftlem8  24979  cvmliftlem10  24981  ghomgrpilem2  25097  fprod2d  25305  faclim  25365  dfpred3  25449  predidm  25463  tz6.26  25480  dftrpred2  25497  bdayfo  25630  pprodcnveq  25728  dfon4  25738  fobigcup  25745  dfiota3  25768  dfrdg4  25795  dfint3  25797  axsegconlem9  25864  ax5seglem7  25874  bpoly2  26103  bpoly3  26104  bpoly4  26105  rankeq1o  26112  ssoninhaus  26198  onint1  26199  rabiun  26236  cnambfre  26255  ftc1anclem8  26287  refssfne  26374  fnopabco  26424  abrexdom  26432  cncfres  26474  mapfzcons  26772  eldioph4b  26872  diophren  26874  rabren3dioph  26876  pwssplit4  27168  dsmmval2  27179  pwfi2f1o  27237  frlmpwfi  27239  psgnunilem2  27395  cnmsgngrp  27413  mendplusgfval  27470  mendmulrfval  27472  mendvscafval  27475  idomodle  27489  cytpval  27505  lhe4.4ex1a  27523  compne  27619  refsum2cnlem1  27684  stoweidlem13  27738  stoweidlem32  27757  stoweidlem62  27787  wallispi2lem2  27797  stirlinglem14  27812  rnfdmpr  28083  swrdccatin1  28205  swrdccat3blem  28218  bnj1400  29207  bnj66  29231  bnj882  29297  cdleme3d  31028  cdleme7a  31040  cdleme31sdnN  31184  cdlemk45  31744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator