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

Theorem eqtr4i 2486
Description: An equality transitivity inference. (Contributed by NM, 26-May-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 2467 . 2  |-  B  =  C
41, 3eqtri 2483 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  3eqtr2i  2489  3eqtr2ri  2490  3eqtr4i  2493  3eqtr4ri  2494  rabab  3124  cbvralcsf  3452  cbvrabcsf  3455  dfin5  3469  dfdif2  3470  uneqin  3746  unrab  3766  inrab  3767  inrab2  3768  difrab  3769  dfrab3ss  3773  rabun2  3774  rabxm  3807  difidALT  3885  difdifdir  3903  dfif3  3943  dfif5  3945  rabsnif  4085  tpidm  4120  ssunpr  4178  sstp  4180  dfint2  4273  iunrab  4362  uniiun  4368  intiin  4369  0iin  4373  mptv  4531  dfepfr  4853  epfrc  4854  xpundi  5041  xpundir  5042  csbcnv  5175  resiun2  5281  resopab  5308  opabresid  5315  dffr3  5357  dfse2  5358  cnvun  5396  imaundir  5404  imainrect  5433  cnvcnv2  5444  cnvcnvres  5454  dmtpop  5467  rnsnopg  5470  rnco2  5497  dmco  5498  co01  5505  unidmrn  5520  dfdm2  5522  dfmpt3  5685  mptun  5694  funcocnv2  5822  dffv2  5921  fnasrn  6053  fpr  6055  fmptap  6070  riotav  6237  dmoprab  6356  rnoprab2  6359  mpt2v  6365  mpt2mptx  6366  abrexex2g  6750  abrexex2  6754  1stval2  6790  2ndval2  6791  fo1st  6793  fo2nd  6794  xp2  6808  dfoprab4f  6831  offval22  6852  fmpt2co  6856  tposmpt2  6984  tposconst  6985  recsfval  7042  rdgsucmpt2  7088  frsucmpt2  7097  df2o3  7135  o1p1e2  7182  oarec  7203  omopthlem2  7297  ecqs  7367  qliftf  7391  erovlem  7399  mapsnf1o3  7460  ixp0x  7490  omf1o  7613  xpf1o  7672  mapunen  7679  enp1ilem  7746  pwfi  7807  marypha1lem  7885  marypha2lem4  7890  dfoi  7928  infeq5i  8044  oemapso  8092  cantnflem1  8099  cantnflem1OLD  8122  rankelop  8283  leweon  8380  r0weon  8381  kmlem11  8531  infcda1  8564  ackbij1lem16  8606  cf0  8622  cfsmolem  8641  alephsuc3  8946  fpwwe  9013  canthp1lem1  9019  wuncval2  9114  prlem936  9414  m1p1sr  9458  m1m1sr  9459  dfcnqs  9508  ssxr  9643  mul02lem2  9746  addid1  9749  3m1e2  10648  2p2e4  10649  3p2e5  10664  3p3e6  10665  4p2e6  10666  4p3e7  10667  4p4e8  10668  5p2e7  10669  5p3e8  10670  5p4e9  10671  5p5e10  10672  6p2e8  10673  6p3e9  10674  6p4e10  10675  7p2e9  10676  7p3e10  10677  8p2e10  10678  nn0suppOLD  10846  nnzrab  10888  nn0zrab  10889  dec0u  10991  dec0h  10992  decsuc  10999  decsucc  11003  numma  11007  decma  11014  decmac  11015  decma2c  11016  decadd  11017  decaddc  11018  decmul1c  11023  decmul2c  11024  5t5e25  11052  6t6e36  11057  8t6e48  11068  nn0uz  11116  nnuz  11117  xaddcom  11440  x2times  11494  ioomax  11602  iccmax  11603  ioopos  11604  ioorp  11605  prunioo  11652  fseq1p1m1  11756  fzo0to2pr  11880  fzo0to3tp  11881  om2uzrdg  12049  fzennn  12060  irec  12249  binom2aiOLD  12260  facnn  12337  fac0  12338  faclbnd2  12351  faclbnd4lem1  12353  hashfun  12479  hashbclem  12485  hashf1lem1  12488  hashf1lem2  12489  fz1isolem  12494  swrdccatin1  12699  swrdccat3blem  12711  s1co  12790  s2eq2s1eq  12872  fsumrev2  13679  fsumparts  13702  fsumiun  13717  isumnn0nn  13736  harmonic  13752  0.999...  13772  fprod2d  13867  ege2le3  13907  cos1bnd  14004  efieq1re  14016  eirrlem  14019  qnnen  14031  cpnnen  14046  ruclem6  14052  3dvds  14134  m1bits  14174  algrp1  14287  phiprmpw  14390  prmreclem4  14521  4sqlem11  14557  4sqlem19  14565  dec5dvds  14634  decsplit1  14652  5prm  14678  7prm  14680  1259lem2  14698  1259lem3  14699  1259lem4  14700  1259lem5  14701  1259prm  14702  2503lem1  14703  2503lem2  14704  2503lem3  14705  2503prm  14706  4001lem1  14707  4001lem2  14708  4001lem3  14709  4001lem4  14710  4001prm  14711  ndxid  14737  strle1  14815  grpbasex  14831  grpplusgx  14832  quslem  15032  xpslem  15062  acsfn1  15150  acsfn2  15152  comfffval2  15189  xpchomfval  15647  xpccofval  15650  1stfval  15659  2ndfval  15662  oduleg  15961  ismgmid  16090  grpinvfvi  16290  gaorb  16544  cntri  16567  cntrsubgnsg  16577  cntrnsg  16578  oppglem  16584  oppgcntr  16599  gsumwrev  16600  symgbas  16604  symgga  16630  cayleylem1  16636  psgnunilem2  16719  efgval2  16941  efgredlemc  16962  efgcpbllema  16971  frgpnabllem1  17076  gsumzaddlem  17133  gsumzaddlemOLD  17135  mgplem  17341  opprlem  17472  oppr0  17477  opprneg  17479  rlmscaf  18049  mplbas  18281  mplbasOLD  18283  mpladd  18299  mplmul  18300  mplvsca2  18303  ressmplbas2  18312  ltbwe  18332  evlslem4OLD  18368  evlslem4  18369  psr1bas2  18424  ply1bas  18429  ply1assa  18433  mplplusg  18456  mplmulr  18457  psr1plusg  18458  psr1vsca  18459  psr1mulr  18460  ply1plusg  18461  ply1vsca  18462  ply1mulr  18463  ply1mpl0  18491  ply1mpl1  18493  coe1mul  18506  xrsds  18656  gsumfsum  18679  zringunit  18703  cnmsgngrp  18788  psgnfix2  18808  relt  18824  ocv0  18881  thlle  18901  thlleval  18902  dsmmval2  18940  frlmip  18980  matgsum  19106  smadiadetglem1  19340  indistpsx  19678  iuncld  19713  tgrest  19827  resstopn  19854  leordtval2  19880  xkouni  20266  ptclsg  20282  ptuncnv  20474  ptunhmeo  20475  alexsubALTlem4  20716  tsmsf1o  20813  ucnimalem  20949  ressxms  21194  uniretop  21435  cnfldtopn  21455  xrtgioo  21477  zcld  21484  icccmp  21496  xrge0gsumle  21504  xrge0tsms  21505  metnrmlem3  21531  fsum2cn  21541  cnmpt2pc  21594  oprpiece1res1  21617  oprpiece1res2  21618  evth  21625  evth2  21626  om1opn  21702  pi1xfrf  21719  pi1xfrcnv  21723  pi1cof  21725  clsocv  21856  cncmet  21927  cnflduss  21962  rrxprds  21987  ehlbase  22004  ismbl  22103  shftmbl  22115  ioorinv  22151  itg1addlem4  22272  itg2cnlem1  22334  iblitg  22341  itg0  22352  itgss3  22387  ditgneg  22427  limcdif  22446  limciun  22464  dvexp  22522  dvef  22547  dvcnvrelem2  22585  ftc1  22609  mdegfvalOLD  22627  plyremlem  22866  aannenlem2  22891  taylply2  22929  dvradcnv  22982  pserdvlem2  22989  reefgim  23011  cospi  23031  sincos6thpi  23074  tanregt0  23092  dflog2  23114  logfac  23154  dvlog  23200  cxpexp  23217  cxpmul2  23238  cxpsqrt  23252  dvsqrt  23286  cxpcn2  23288  ang180lem2  23341  isosctrlem2  23350  1cubrlem  23369  1cubr  23370  quart1lem  23383  atancj  23438  atanlogaddlem  23441  atansopn  23460  leibpilem2  23469  log2cnv  23472  log2ublem3  23476  birthdaylem1  23479  birthdaylem2  23480  birthday  23482  dfarea  23488  wilthlem2  23541  ftalem3  23546  ftalem7  23550  basellem2  23553  ppiprm  23623  ppinprm  23624  chtprm  23625  chtnprm  23626  ppi2  23642  ppi3  23643  ppiub  23677  chtub  23685  bclbnd  23753  bposlem8  23764  lgsdilem  23795  lgsdir2lem1  23796  lgsdir2lem2  23797  lgsdir2lem3  23798  lgsquadlem2  23828  lgsquad2lem2  23832  rplogsum  23910  mulog2sumlem2  23918  pnt2  23996  istrkg2ld  24056  axsegconlem9  24430  ax5seglem7  24440  usgrares1  24612  cusgrares  24674  wwlknprop  24888  wwlknfi  24940  wlknwwlknvbij  24942  clwwlkvbij  25003  eupath2lem3  25181  konigsberg  25189  ex-pw  25352  ex-xp  25359  ex-rn  25363  ablosn  25547  efghgrpOLD  25573  nvvop  25700  nvm  25734  cnims  25801  ip0i  25938  ip1ilem  25939  ipdirilem  25942  ipasslem10  25952  h2hva  26089  h2hsm  26090  h2hvs  26092  axhfvadd-zf  26097  axhvcom-zf  26098  axhvass-zf  26099  axhv0cl-zf  26100  axhvaddid-zf  26101  axhfvmul-zf  26102  axhvmulid-zf  26103  axhvmulass-zf  26104  axhvdistr1-zf  26105  axhvdistr2-zf  26106  axhvmul0-zf  26107  axhfi-zf  26108  axhis1-zf  26109  axhis2-zf  26110  axhis3-zf  26111  axhis4-zf  26112  axhcompl-zf  26113  normlem0  26224  normlem1  26225  normlem2  26226  normlem4  26228  normlem9  26233  bcseqi  26235  dfhnorm2  26237  norm3difi  26262  normpari  26269  normpar2i  26271  polid2i  26272  polidi  26273  hhba  26282  hhims  26287  hhims2  26288  hhsssh  26383  hhssims  26389  hhssims2  26390  shsval3i  26504  dfch2  26523  cmcm2i  26709  fh2  26735  qlaxr3i  26752  spansnji  26762  pjcji  26800  ho0val  26867  df0op2  26869  hosd1i  26939  hosd2i  26940  eigorthi  26954  hhlnoi  27017  hhnmoi  27018  hhbloi  27019  bra0  27067  nmop0  27103  nmfn0  27104  lnopeq0lem1  27122  lnopunilem1  27127  lnophmlem2  27134  nmopcoadji  27218  pjhmopidm  27300  cvmdi  27441  cdj3lem3  27555  cdj3lem3b  27557  abrexdomjm  27604  iundifdifd  27639  iundifdif  27640  mpt2mptxf  27746  df1stres  27750  df2ndres  27751  fcobijfs  27780  resf1o  27784  fpwrelmapffslem  27786  xrslt  27898  xrsclat  27902  gsumle  28004  xrge0tsmsd  28010  xrge0slmod  28069  fimaproj  28071  circtopn  28075  tpr2rico  28129  xrge0mulc1cn  28158  lmxrge0  28169  esumpfinvallem  28303  esumcocn  28309  hasheuni  28314  esumcvg  28315  measinblem  28428  aean  28453  sxbrsigalem3  28480  dya2iocival  28481  dya2iocucvr  28492  sxbrsigalem1  28493  sxbrsigalem2  28494  sxbrsigalem5  28496  sxbrsiga  28498  fiunelcarsg  28524  eulerpartlem1  28570  eulerpartgbij  28575  fibp1  28604  coinfliplem  28681  coinflipprob  28682  ballotlemfval  28692  ballotth  28740  sgnneg  28743  ofs2  28765  plymulx  28769  lgamgulmlem5  28839  lgambdd  28843  derang0  28877  subfacp1lem1  28887  subfacp1lem6  28893  kur14lem7  28920  cvmsss2  28983  cvmliftlem8  29001  cvmliftlem10  29003  msubfval  29148  quad3  29288  ghomgrpilem2  29290  faclim  29412  predidm  29508  tz6.26  29525  dftrpred2  29542  bdayfo  29675  pprodcnveq  29761  dfon4  29771  fobigcup  29778  dfiota3  29801  dfrdg4  29828  dfint3  29830  bpoly2  30047  bpoly3  30048  bpoly4  30049  rankeq1o  30056  ssoninhaus  30141  onint1  30142  rabiun  30276  ptrest  30288  cnambfre  30303  ftc1anclem8  30337  dvcnsqrt  30341  refssfne  30416  fnopabco  30453  abrexdom  30461  cncfres  30501  scottexf  30816  scott0f  30817  mapfzcons  30888  eldioph4b  30984  diophren  30986  pwssplit4  31274  pwfi2f1o  31283  pwfi2f1oOLD  31284  frlmpwfi  31287  mendplusgfval  31375  mendmulrfval  31377  mendvscafval  31380  idomodle  31394  cytpval  31410  arearect  31424  nznngen  31462  hashnzfz2  31467  lhe4.4ex1a  31475  dvradcnv2  31493  binomcxplemrat  31496  binomcxplemnotnn0  31502  compne  31590  refsum2cnlem1  31652  rnmptc  31689  iccdifprioo  31795  lptre2pt  31885  limclner  31896  stoweidlem13  32034  stoweidlem32  32053  stoweidlem62  32083  wallispi2lem2  32093  stirlinglem14  32108  dirkertrigeqlem1  32119  dirkercncflem4  32127  fourierdlem42  32170  fourierdlem73  32201  fourierdlem81  32209  fourierdlem92  32220  fourierdlem103  32231  fourierdlem104  32232  fouriercnp  32248  fouriersw  32253  opoeALTV  32589  rnfdmpr  32682  cznabel  33016  cznrng  33017  mpt2mptx2  33178  bnj1400  34295  bnj66  34319  bnj882  34385  bj-rababwv  34844  cdleme3d  36353  cdleme7a  36365  cdleme31sdnN  36510  cdlemk45  37070  dfrcl3  38194  dfid5  38195  dfid6  38196  dfrcl4  38197  comptiunov2i  38216  corcltrcl  38231  inductionexd  38419
  Copyright terms: Public domain W3C validator