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

Theorem eqtr4i 2431
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 2412 . 2  |-  B  =  C
41, 3eqtri 2428 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  3eqtr2i  2434  3eqtr2ri  2435  3eqtr4i  2438  3eqtr4ri  2439  rabab  2937  cbvralcsf  3275  cbvrabcsf  3278  dfin5  3292  dfdif2  3293  uneqin  3556  unrab  3576  inrab  3577  inrab2  3578  difrab  3579  dfrab3ss  3583  rabun2  3584  rabxm  3614  difidALT  3661  difdifdir  3679  dfif3  3713  dfif5  3715  tpidm  3872  ssunpr  3925  sstp  3927  dfint2  4016  iunrab  4102  uniiun  4108  intiin  4109  0iin  4113  mptv  4265  dfepfr  4531  epfrc  4532  xpundi  4893  xpundir  4894  resiun2  5129  resopab  5150  opabresid  5157  dffr3  5199  dfse2  5200  cnvun  5240  imaundir  5248  imainrect  5275  cnvcnv2  5287  cnvcnvres  5296  dmtpop  5309  rnsnopg  5312  rnco2  5340  dmco  5341  co01  5347  unidmrn  5362  dfdm2  5364  dfmpt3  5530  mptun  5538  funcocnv2  5663  dffv2  5759  fnasrn  5875  fpr  5877  fmptap  5886  abrexex2g  5951  abrexex2  5964  dmoprab  6117  rnoprab2  6120  mpt2v  6126  mpt2mptx  6127  1stval2  6327  2ndval2  6328  fo1st  6329  fo2nd  6330  xp2  6347  dfoprab4f  6368  fmpt2co  6393  tposmpt2  6479  riotav  6517  cbvriota  6523  recsfval  6605  rdgsucmpt2  6651  frsucmpt2  6660  df2o3  6700  o1p1e2  6747  oarec  6768  omopthlem2  6862  ecqs  6931  qliftf  6955  erovlem  6963  mapsnf1o3  7025  ixp0x  7053  omf1o  7174  xpf1o  7232  mapunen  7239  enp1ilem  7305  pwfi  7364  marypha1lem  7400  marypha2lem4  7405  dfoi  7440  infeq5i  7551  oemapso  7598  cantnflem1  7605  rankelop  7760  leweon  7853  r0weon  7854  kmlem11  8000  infcda1  8033  ackbij1lem16  8075  cf0  8091  cfsmolem  8110  alephsuc3  8415  fpwwe  8481  canthp1lem1  8487  wuncval2  8582  prlem936  8884  m1p1sr  8927  m1m1sr  8928  dfcnqs  8977  ssxr  9105  mul02lem2  9203  addid1  9206  3m1e2  10056  3m1e2OLD  10057  2p2e4  10058  3p2e5  10071  3p3e6  10072  4p2e6  10073  4p3e7  10074  4p4e8  10075  5p2e7  10076  5p3e8  10077  5p4e9  10078  5p5e10  10079  6p2e8  10080  6p3e9  10081  6p4e10  10082  7p2e9  10083  7p3e10  10084  8p2e10  10085  nn0supp  10233  nnzrab  10269  nn0zrab  10270  dec0u  10357  dec0h  10358  decsuc  10365  decsucc  10369  numma  10373  decma  10380  decmac  10381  decma2c  10382  decadd  10383  decaddc  10384  decmul1c  10389  decmul2c  10390  5t5e25  10418  6t6e36  10423  8t6e48  10434  nn0uz  10480  nnuz  10481  xaddcom  10784  x2times  10838  ioomax  10945  iccmax  10946  ioopos  10947  ioorp  10948  prunioo  10985  fseq1p1m1  11081  fzo0to2pr  11143  fzo0to3tp  11144  om2uzrdg  11255  fzennn  11266  irec  11439  binom2aiOLD  11450  facnn  11527  fac0  11528  faclbnd2  11541  faclbnd4lem1  11543  hashfun  11659  hashbclem  11660  hashf1lem1  11663  hashf1lem2  11664  fz1isolem  11669  s1co  11761  fsumrev2  12524  fsumparts  12544  fsumiun  12559  isumnn0nn  12581  harmonic  12597  0.999...  12617  ege2le3  12651  cos1bnd  12747  efieq1re  12759  eirrlem  12762  qnnen  12772  cpnnen  12787  ruclem6  12793  3dvds  12871  m1bits  12911  algrp1  13024  phiprmpw  13124  prmreclem4  13246  4sqlem11  13282  4sqlem19  13290  dec5dvds  13359  decsplit1  13377  5prm  13390  7prm  13392  1259lem2  13410  1259lem3  13411  1259lem4  13412  1259lem5  13413  1259prm  13414  2503lem1  13415  2503lem2  13416  2503lem3  13417  2503prm  13418  4001lem1  13419  4001lem2  13420  4001lem3  13421  4001lem4  13422  4001prm  13423  ndxid  13449  strle1  13519  grpbasex  13531  grpplusgx  13532  divslem  13727  xpslem  13757  acsfn1  13845  acsfn2  13847  comfffval2  13886  xpchomfval  14235  xpccofval  14238  1stfval  14247  2ndfval  14250  oduleg  14518  grpinvfvi  14805  gaorb  15043  symgbas  15054  symgga  15068  cayleylem1  15069  cntri  15088  cntrsubgnsg  15098  cntrnsg  15099  oppglem  15105  oppgcntr  15120  gsumwrev  15121  efgval2  15315  efgredlemc  15336  efgcpbllema  15345  frgpnabllem1  15443  gsumzaddlem  15485  mgplem  15612  opprlem  15692  oppr0  15697  opprneg  15699  rlmscaf  16238  mplbas  16452  mpladd  16464  mplmul  16465  mplvsca2  16468  ressmplbas2  16477  ltbwe  16492  evlslem4  16523  psr1bas2  16547  ply1bas  16552  ply1assa  16556  mplplusg  16573  mplmulr  16574  psr1plusg  16575  psr1vsca  16576  psr1mulr  16577  ply1plusg  16578  ply1vsca  16579  ply1mulr  16580  ply1mpl0  16608  ply1mpl1  16609  coe1mul  16622  xrsds  16700  zrngunit  16724  gsumfsum  16725  ocv0  16863  thlle  16883  thlleval  16884  indistpsx  17033  iuncld  17068  tgrest  17181  resstopn  17208  leordtval2  17234  xkouni  17588  ptclsg  17604  ptuncnv  17796  ptunhmeo  17797  alexsubALTlem4  18038  tsmsf1o  18131  ucnimalem  18267  ressxms  18512  uniretop  18753  cnfldtopn  18773  xrtgioo  18794  zcld  18801  icccmp  18813  xrge0gsumle  18821  xrge0tsms  18822  metnrmlem3  18848  fsum2cn  18858  cnmpt2pc  18910  oprpiece1res1  18933  oprpiece1res2  18934  evth  18941  evth2  18942  om1opn  19018  pi1xfrf  19035  pi1xfrcnv  19039  pi1cof  19041  clsocv  19161  cncmet  19232  cnflduss  19267  ismbl  19379  shftmbl  19390  ioorinv  19425  itg1addlem4  19548  itg2cnlem1  19610  iblitg  19617  itg0  19628  itgss3  19663  ditgneg  19701  limcdif  19720  limciun  19738  dvexp  19796  dvef  19821  dvcnvrelem2  19859  ftc1  19883  plyremlem  20178  aannenlem2  20203  taylply2  20241  dvradcnv  20294  pserdvlem2  20301  reefgim  20323  cospi  20337  sincos6thpi  20380  tanregt0  20398  dflog2  20415  logfac  20452  dvlog  20499  cxpexp  20516  cxpmul2  20537  cxpsqr  20551  dvsqr  20585  cxpcn2  20587  ang180lem2  20609  isosctrlem2  20620  1cubrlem  20638  1cubr  20639  quart1lem  20652  atancj  20707  atanlogaddlem  20710  atansopn  20729  leibpilem2  20738  log2cnv  20741  log2ublem3  20745  birthdaylem1  20747  birthdaylem2  20748  birthday  20750  dfarea  20756  wilthlem2  20809  ftalem3  20814  ftalem7  20818  basellem2  20821  ppiprm  20891  ppinprm  20892  chtprm  20893  chtnprm  20894  ppi2  20910  ppi3  20911  ppiub  20945  chtub  20953  bclbnd  21021  bposlem8  21032  lgsdilem  21063  lgsdir2lem1  21064  lgsdir2lem2  21065  lgsdir2lem3  21066  lgsquadlem2  21096  lgsquad2lem2  21100  rplogsum  21178  mulog2sumlem2  21186  pnt2  21264  usgrares1  21381  cusgrares  21438  eupath2lem3  21658  konigsberg  21666  ex-pw  21694  ex-xp  21701  ex-rn  21705  ablosn  21892  efghgrp  21918  nvvop  22045  nvm  22079  cnims  22146  ip0i  22283  ip1ilem  22284  ipdirilem  22287  ipasslem10  22297  h2hva  22434  h2hsm  22435  h2hvs  22437  axhfvadd-zf  22442  axhvcom-zf  22443  axhvass-zf  22444  axhv0cl-zf  22445  axhvaddid-zf  22446  axhfvmul-zf  22447  axhvmulid-zf  22448  axhvmulass-zf  22449  axhvdistr1-zf  22450  axhvdistr2-zf  22451  axhvmul0-zf  22452  axhfi-zf  22453  axhis1-zf  22454  axhis2-zf  22455  axhis3-zf  22456  axhis4-zf  22457  axhcompl-zf  22458  normlem0  22568  normlem1  22569  normlem2  22570  normlem4  22572  normlem9  22577  bcseqi  22579  dfhnorm2  22581  norm3difi  22606  normpari  22613  normpar2i  22615  polid2i  22616  polidi  22617  hhba  22626  hhims  22631  hhims2  22632  hhsssh  22726  hhssims  22732  hhssims2  22733  shsval3i  22847  dfch2  22866  cmcm2i  23052  fh2  23078  qlaxr3i  23095  spansnji  23105  pjcji  23143  ho0val  23210  df0op2  23212  hosd1i  23282  hosd2i  23283  eigorthi  23297  hhlnoi  23360  hhnmoi  23361  hhbloi  23362  bra0  23410  nmop0  23446  nmfn0  23447  lnopeq0lem1  23465  lnopunilem1  23470  lnophmlem2  23477  nmopcoadji  23561  pjhmopidm  23643  cvmdi  23784  cdj3lem3  23898  cdj3lem3b  23900  abrexdomjm  23945  iundifdifd  23969  iundifdif  23970  df1stres  24048  df2ndres  24049  xrslt  24155  xrge0tsmsd  24180  relt  24233  tpr2rico  24267  xrge0mulc1cn  24284  lmxrge0  24294  esumpfinvallem  24421  esumcocn  24427  hasheuni  24432  esumcvg  24433  measinblem  24531  aean  24552  sxbrsigalem3  24579  dya2iocival  24580  dya2iocucvr  24591  sxbrsigalem1  24592  sxbrsigalem2  24593  sxbrsigalem5  24595  sxbrsiga  24597  sitgclbn  24614  coinfliplem  24693  coinflipprob  24694  ballotlemfval  24704  ballotth  24752  lgamgulmlem5  24774  lgambdd  24778  derang0  24812  subfacp1lem1  24822  subfacp1lem6  24828  kur14lem7  24855  cvmsss2  24918  cvmliftlem8  24936  cvmliftlem10  24938  ghomgrpilem2  25054  fprod2d  25262  faclim  25317  predidm  25406  tz6.26  25423  dftrpred2  25440  bdayfo  25547  pprodcnveq  25641  dfon4  25651  fobigcup  25658  dfiota3  25680  dfrdg4  25707  axsegconlem9  25772  ax5seglem7  25782  bpoly2  26011  bpoly3  26012  bpoly4  26013  rankeq1o  26020  ssoninhaus  26106  onint1  26107  rabiun2  26143  cnambfre  26158  refssfne  26268  fnopabco  26318  abrexdom  26326  cncfres  26368  mapfzcons  26666  eldioph4b  26766  diophren  26768  rabren3dioph  26770  pwssplit4  27063  dsmmval2  27074  pwfi2f1o  27132  frlmpwfi  27134  psgnunilem2  27290  cnmsgngrp  27308  mendplusgfval  27365  mendmulrfval  27367  mendvscafval  27370  idomodle  27384  cytpval  27400  lhe4.4ex1a  27418  compne  27514  refsum2cnlem1  27579  stoweidlem13  27633  stoweidlem32  27652  stoweidlem62  27682  wallispi2lem2  27692  stirlinglem14  27707  rnfdmpr  27968  swrdccatin1  28020  bnj1400  28917  bnj66  28941  bnj882  29007  cdleme3d  30717  cdleme7a  30729  cdleme31sdnN  30873  cdlemk45  31433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2401
  Copyright terms: Public domain W3C validator