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

Theorem eqtr4i 2306
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 2287 . 2  |-  B  =  C
41, 3eqtri 2303 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  3eqtr2i  2309  3eqtr2ri  2310  3eqtr4i  2313  3eqtr4ri  2314  rabab  2805  cbvralcsf  3143  cbvrabcsf  3146  dfin5  3160  dfdif2  3161  uneqin  3420  unrab  3439  inrab  3440  inrab2  3441  difrab  3442  dfrab3ss  3446  rabun2  3447  rabxm  3477  difidALT  3523  difdifdir  3541  dfif3  3575  dfif5  3577  tpidm  3731  ssunpr  3776  sstp  3778  dfint2  3864  iunrab  3949  uniiun  3955  intiin  3956  0iin  3960  mptv  4112  dfepfr  4378  epfrc  4379  xpundi  4741  xpundir  4742  resiundiOLD  4745  resiun2  4975  resopab  4996  opabresid  5003  dffr3  5045  dfse2  5046  cnvun  5086  imaundir  5094  imainrect  5119  cnvcnv2  5127  cnvcnvres  5136  dmtpop  5149  rnsnopg  5152  rnco2  5180  dmco  5181  co01  5187  unidmrn  5202  dfdm2  5204  dfmpt3  5366  mptun  5374  funcocnv2  5498  dffv2  5592  fnasrn  5702  fpr  5704  fmptap  5710  abrexex2g  5768  abrexex2  5780  dmoprab  5928  rnoprab2  5931  mpt2v  5937  mpt2mptx  5938  1stval2  6137  2ndval2  6138  fo1st  6139  fo2nd  6140  xp2  6157  dfoprab4f  6178  fmpt2co  6202  tposmpt2  6271  riotav  6309  cbvriota  6315  recsfval  6397  rdgsucmpt2  6443  frsucmpt2  6452  df2o3  6492  o1p1e2  6539  oarec  6560  omopthlem2  6654  ecqs  6723  qliftf  6746  erovlem  6754  mapsnf1o3  6816  ixp0x  6844  omf1o  6965  xpf1o  7023  mapunen  7030  enp1ilem  7092  pwfi  7151  marypha1lem  7186  marypha2lem4  7191  dfoi  7226  infeq5i  7337  oemapso  7384  cantnflem1  7391  rankelop  7546  leweon  7639  r0weon  7640  kmlem11  7786  infcda1  7819  ackbij1lem16  7861  cf0  7877  cfsmolem  7896  alephsuc3  8202  fpwwe  8268  canthp1lem1  8274  wuncval2  8369  prlem936  8671  m1p1sr  8714  m1m1sr  8715  dfcnqs  8764  ssxr  8892  mul02lem2  8989  addid1  8992  2p2e4  9842  3p2e5  9855  3p3e6  9856  4p2e6  9857  4p3e7  9858  4p4e8  9859  5p2e7  9860  5p3e8  9861  5p4e9  9862  5p5e10  9863  6p2e8  9864  6p3e9  9865  6p4e10  9866  7p2e9  9867  7p3e10  9868  8p2e10  9869  nn0supp  10017  nnzrab  10051  nn0zrab  10052  dec0u  10139  dec0h  10140  decsuc  10147  decsucc  10151  numma  10155  decma  10162  decmac  10163  decma2c  10164  decadd  10165  decaddc  10166  decmul1c  10171  decmul2c  10172  5t5e25  10200  6t6e36  10205  8t6e48  10216  nn0uz  10262  nnuz  10263  xaddcom  10565  x2times  10619  ioomax  10724  iccmax  10725  ioopos  10726  ioorp  10727  prunioo  10764  fseq1p1m1  10857  om2uzrdg  11019  fzennn  11030  irec  11202  binom2aiOLD  11213  facnn  11290  fac0  11291  faclbnd2  11304  faclbnd4lem1  11306  hashfun  11389  hashbclem  11390  hashf1lem1  11393  hashf1lem2  11394  fz1isolem  11399  s1co  11488  fsumrev2  12244  fsumparts  12264  fsumiun  12279  isumnn0nn  12301  harmonic  12317  0.999...  12337  ege2le3  12371  cos1bnd  12467  efieq1re  12479  eirrlem  12482  qnnen  12492  cpnnen  12507  ruclem6  12513  3dvds  12591  m1bits  12631  algrp1  12744  phiprmpw  12844  prmreclem4  12966  4sqlem11  13002  4sqlem19  13010  dec5dvds  13079  decsplit1  13097  5prm  13110  7prm  13112  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  ndxid  13169  strle1  13239  grpbasex  13251  grpplusgx  13252  divslem  13445  xpslem  13475  acsfn1  13563  acsfn2  13565  comfffval2  13604  oppchomf  13623  xpchomfval  13953  xpccofval  13956  1stfval  13965  2ndfval  13968  oduleg  14236  grpinvfvi  14523  gaorb  14761  symgbas  14772  symgga  14786  cayleylem1  14787  cntri  14806  cntrsubgnsg  14816  cntrnsg  14817  oppglem  14823  oppgcntr  14838  gsumwrev  14839  efgval2  15033  efgredlemc  15054  efgcpbllema  15063  frgpnabllem1  15161  gsumzaddlem  15203  mgplem  15330  opprlem  15410  oppr0  15415  opprneg  15417  rlmscaf  15960  mplbas  16174  mpladd  16186  mplmul  16187  mplvsca2  16190  ressmplbas2  16199  ltbwe  16214  evlslem4  16245  psr1bas2  16269  ply1bas  16274  ply1assa  16278  mplplusg  16297  mplvscafvalOLD  16298  mplmulr  16299  psr1plusg  16300  psr1vsca  16301  psr1mulr  16302  ply1plusg  16303  ply1vsca  16304  ply1mulr  16305  ply1mpl0  16333  ply1mpl1  16334  coe1mul  16347  xrsds  16414  zrngunit  16438  gsumfsum  16439  ocv0  16577  thlle  16597  thlleval  16598  indistpsx  16747  iuncld  16782  tgrest  16890  resstopn  16916  leordtval2  16942  xkouni  17294  ptclsg  17309  ptuncnv  17498  ptunhmeo  17499  alexsubALTlem4  17744  tsmsf1o  17827  ressxms  18071  uniretop  18271  cnfldtopn  18291  xrtgioo  18312  zcld  18319  icccmp  18330  xrge0gsumle  18338  xrge0tsms  18339  metnrmlem3  18365  fsum2cn  18375  cnmpt2pc  18426  oprpiece1res1  18449  oprpiece1res2  18450  evth  18457  evth2  18458  om1opn  18534  pi1xfrf  18551  pi1xfrcnv  18555  pi1cof  18557  clsocv  18677  cncmet  18744  ismbl  18885  shftmbl  18896  ioorinv  18931  itg1addlem4  19054  itg2cnlem1  19116  iblitg  19123  itg0  19134  itgss3  19169  ditgneg  19207  limcdif  19226  limciun  19244  dvexp  19302  dvef  19327  dvcnvrelem2  19365  ftc1  19389  plyremlem  19684  aannenlem2  19709  taylply2  19747  dvradcnv  19797  pserdvlem2  19804  reefgim  19826  cospi  19840  sincos6thpi  19883  tanregt0  19901  dflog2  19918  logfac  19954  dvlog  19998  cxpexp  20015  cxpmul2  20036  cxpsqr  20050  dvsqr  20084  cxpcn2  20086  ang180lem2  20108  isosctrlem2  20119  1cubrlem  20137  1cubr  20138  quart1lem  20151  atancj  20206  atanlogaddlem  20209  atansopn  20228  leibpilem2  20237  log2cnv  20240  log2ublem3  20244  birthdaylem1  20246  birthdaylem2  20247  birthday  20249  dfarea  20255  wilthlem2  20307  ftalem3  20312  ftalem7  20316  basellem2  20319  ppiprm  20389  ppinprm  20390  chtprm  20391  chtnprm  20392  ppi2  20408  ppi3  20409  ppiub  20443  chtub  20451  bclbnd  20519  bposlem8  20530  lgsdilem  20561  lgsdir2lem1  20562  lgsdir2lem2  20563  lgsdir2lem3  20564  lgsquadlem2  20594  lgsquad2lem2  20598  rplogsum  20676  mulog2sumlem2  20684  pnt2  20762  ex-pw  20816  ex-xp  20823  ex-rn  20827  ablosn  21014  efghgrp  21040  nvvop  21165  nvm  21199  cnims  21266  ip0i  21403  ip1ilem  21404  ipdirilem  21407  ipasslem10  21417  h2hva  21554  h2hsm  21555  h2hvs  21557  axhfvadd-zf  21562  axhvcom-zf  21563  axhvass-zf  21564  axhv0cl-zf  21565  axhvaddid-zf  21566  axhfvmul-zf  21567  axhvmulid-zf  21568  axhvmulass-zf  21569  axhvdistr1-zf  21570  axhvdistr2-zf  21571  axhvmul0-zf  21572  axhfi-zf  21573  axhis1-zf  21574  axhis2-zf  21575  axhis3-zf  21576  axhis4-zf  21577  axhcompl-zf  21578  normlem0  21688  normlem1  21689  normlem2  21690  normlem4  21692  normlem9  21697  bcseqi  21699  dfhnorm2  21701  norm3difi  21726  normpari  21733  normpar2i  21735  polid2i  21736  polidi  21737  hhba  21746  hhims  21751  hhims2  21752  hhsssh  21846  hhssims  21852  hhssims2  21853  shsval3i  21967  dfch2  21986  cmcm2i  22172  fh2  22198  qlaxr3i  22215  spansnji  22225  pjcji  22263  ho0val  22330  df0op2  22332  hosd1i  22402  hosd2i  22403  eigorthi  22417  hhlnoi  22480  hhnmoi  22481  hhbloi  22482  bra0  22530  nmop0  22566  nmfn0  22567  lnopeq0lem1  22585  lnopunilem1  22590  lnophmlem2  22597  nmopcoadji  22681  pjhmopidm  22763  cvmdi  22904  cdj3lem3  23018  cdj3lem3b  23020  ballotlemfval  23048  ballotth  23096  iundifdifd  23159  iundifdif  23160  abrexdomjm  23165  df1stres  23243  df2ndres  23244  tpr2rico  23296  xrge0mulc1cn  23323  lmxrge0  23375  xrge0tsmsd  23382  esumpfinvallem  23442  esumcocn  23448  hasheuni  23453  esumcvg  23454  measinblem  23547  dya2iocival  23576  dya2iocrrnval  23582  coinfliplem  23679  coinflipprob  23680  derang0  23700  subfacp1lem1  23710  subfacp1lem6  23716  kur14lem7  23743  cvmsss2  23805  cvmliftlem8  23823  cvmliftlem10  23825  eupath2lem3  23903  konigsberg  23911  ghomgrpilem2  23993  predidm  24188  tz6.26  24205  dftrpred2  24222  bdayfo  24329  pprodcnveq  24423  dfon4  24433  fobigcup  24440  dfiota3  24462  dfrdg4  24488  axsegconlem9  24553  ax5seglem7  24563  axlowdimlem16  24585  bpoly2  24792  bpoly3  24793  bpoly4  24794  rankeq1o  24801  ssoninhaus  24887  onint1  24888  clsbldimp  25088  2eq3m1  25179  vecval3b  25452  islimrs4  25582  trnij  25615  nolimf  25619  flfnein  25621  jdmo  25778  refssfne  26294  fnopabco  26388  abrexdom  26405  cncfres  26485  mapfzcons  26793  eldioph4b  26894  diophren  26896  rabren3dioph  26898  pwssplit4  27191  dsmmval2  27202  pwfi2f1o  27260  frlmpwfi  27262  psgnunilem2  27418  cnmsgngrp  27436  mendplusgfval  27493  mendmulrfval  27495  mendvscafval  27498  idomodle  27512  cytpval  27528  lhe4.4ex1a  27546  compne  27642  refsum2cnlem1  27708  stoweidlem13  27762  stoweidlem32  27781  stoweidlem62  27811  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem3  27825  bnj1400  28868  bnj66  28892  bnj882  28958  cdleme3d  30420  cdleme7a  30432  cdleme31sdnN  30576  cdlemk45  31136
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator