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

Theorem eqtr4i 2473
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 2454 . 2  |-  B  =  C
41, 3eqtri 2470 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-cleq 2433
This theorem is referenced by:  3eqtr2i  2476  3eqtr2ri  2477  3eqtr4i  2480  3eqtr4ri  2481  rabab  3111  cbvralcsf  3450  cbvrabcsf  3453  dfin5  3467  dfdif2  3468  uneqin  3732  unrab  3752  inrab  3753  inrab2  3754  difrab  3755  dfrab3ss  3759  rabun2  3760  rabxm  3791  difidALT  3880  difdifdir  3898  dfif3  3937  dfif5  3939  rabsnif  4081  tpidm  4116  ssunpr  4174  sstp  4176  dfint2  4270  iunrab  4359  uniiun  4365  intiin  4366  0iin  4370  mptv  4526  dfepfr  4851  epfrc  4852  xpundi  5039  xpundir  5040  csbcnv  5173  resiun2  5280  resopab  5307  opabresid  5314  dffr3  5356  dfse2  5357  cnvun  5398  imaundir  5406  imainrect  5435  cnvcnv2  5447  cnvcnvres  5458  dmtpop  5471  rnsnopg  5474  rnco2  5501  dmco  5502  co01  5509  unidmrn  5524  dfdm2  5526  dfmpt3  5690  mptun  5699  funcocnv2  5827  dffv2  5928  fnasrn  6059  fpr  6061  fmptap  6076  riotav  6244  dmoprab  6365  rnoprab2  6368  mpt2v  6374  mpt2mptx  6375  abrexex2g  6759  abrexex2  6763  1stval2  6799  2ndval2  6800  fo1st  6802  fo2nd  6803  xp2  6817  dfoprab4f  6840  offval22  6861  fmpt2co  6865  tposmpt2  6991  tposconst  6992  recsfval  7049  rdgsucmpt2  7095  frsucmpt2  7104  df2o3  7142  o1p1e2  7189  oarec  7210  omopthlem2  7304  ecqs  7374  qliftf  7398  erovlem  7406  mapsnf1o3  7466  ixp0x  7496  omf1o  7619  xpf1o  7678  mapunen  7685  enp1ilem  7753  pwfi  7814  marypha1lem  7892  marypha2lem4  7897  dfoi  7936  infeq5i  8053  oemapso  8101  cantnflem1  8108  cantnflem1OLD  8131  rankelop  8292  leweon  8389  r0weon  8390  kmlem11  8540  infcda1  8573  ackbij1lem16  8615  cf0  8631  cfsmolem  8650  alephsuc3  8955  fpwwe  9024  canthp1lem1  9030  wuncval2  9125  prlem936  9425  m1p1sr  9469  m1m1sr  9470  dfcnqs  9519  ssxr  9654  mul02lem2  9757  addid1  9760  3m1e2  10655  2p2e4  10656  3p2e5  10671  3p3e6  10672  4p2e6  10673  4p3e7  10674  4p4e8  10675  5p2e7  10676  5p3e8  10677  5p4e9  10678  5p5e10  10679  6p2e8  10680  6p3e9  10681  6p4e10  10682  7p2e9  10683  7p3e10  10684  8p2e10  10685  nn0suppOLD  10853  nnzrab  10895  nn0zrab  10896  dec0u  10996  dec0h  10997  decsuc  11004  decsucc  11008  numma  11012  decma  11019  decmac  11020  decma2c  11021  decadd  11022  decaddc  11023  decmul1c  11028  decmul2c  11029  5t5e25  11057  6t6e36  11062  8t6e48  11073  nn0uz  11121  nnuz  11122  xaddcom  11443  x2times  11497  ioomax  11605  iccmax  11606  ioopos  11607  ioorp  11608  prunioo  11655  fseq1p1m1  11758  fzo0to2pr  11875  fzo0to3tp  11876  om2uzrdg  12043  fzennn  12054  irec  12243  binom2aiOLD  12254  facnn  12331  fac0  12332  faclbnd2  12345  faclbnd4lem1  12347  hashfun  12471  hashbclem  12477  hashf1lem1  12480  hashf1lem2  12481  fz1isolem  12486  swrdccatin1  12684  swrdccat3blem  12696  s1co  12775  s2eq2s1eq  12857  fsumrev2  13573  fsumparts  13596  fsumiun  13611  isumnn0nn  13630  harmonic  13646  0.999...  13666  ege2le3  13700  cos1bnd  13796  efieq1re  13808  eirrlem  13811  qnnen  13821  cpnnen  13836  ruclem6  13842  3dvds  13924  m1bits  13964  algrp1  14077  phiprmpw  14180  prmreclem4  14311  4sqlem11  14347  4sqlem19  14355  dec5dvds  14424  decsplit1  14442  5prm  14468  7prm  14470  1259lem2  14488  1259lem3  14489  1259lem4  14490  1259lem5  14491  1259prm  14492  2503lem1  14493  2503lem2  14494  2503lem3  14495  2503prm  14496  4001lem1  14497  4001lem2  14498  4001lem3  14499  4001lem4  14500  4001prm  14501  ndxid  14527  strle1  14602  grpbasex  14614  grpplusgx  14615  quslem  14814  xpslem  14844  acsfn1  14932  acsfn2  14934  comfffval2  14970  xpchomfval  15319  xpccofval  15322  1stfval  15331  2ndfval  15334  oduleg  15633  ismgmid  15762  grpinvfvi  15962  gaorb  16216  cntri  16239  cntrsubgnsg  16249  cntrnsg  16250  oppglem  16256  oppgcntr  16271  gsumwrev  16272  symgbas  16276  symgga  16302  cayleylem1  16308  psgnunilem2  16391  efgval2  16613  efgredlemc  16634  efgcpbllema  16643  frgpnabllem1  16748  gsumzaddlem  16805  gsumzaddlemOLD  16807  mgplem  17017  opprlem  17148  oppr0  17153  opprneg  17155  rlmscaf  17725  mplbas  17957  mplbasOLD  17959  mpladd  17975  mplmul  17976  mplvsca2  17979  ressmplbas2  17988  ltbwe  18008  evlslem4OLD  18044  evlslem4  18045  psr1bas2  18100  ply1bas  18105  ply1assa  18109  mplplusg  18132  mplmulr  18133  psr1plusg  18134  psr1vsca  18135  psr1mulr  18136  ply1plusg  18137  ply1vsca  18138  ply1mulr  18139  ply1mpl0  18167  ply1mpl1  18169  coe1mul  18182  xrsds  18332  gsumfsum  18355  zringunit  18390  zrngunit  18391  cnmsgngrp  18485  psgnfix2  18505  relt  18521  ocv0  18578  thlle  18598  thlleval  18599  dsmmval2  18637  frlmip  18679  matgsum  18809  smadiadetglem1  19043  indistpsx  19381  iuncld  19416  tgrest  19530  resstopn  19557  leordtval2  19583  xkouni  19970  ptclsg  19986  ptuncnv  20178  ptunhmeo  20179  alexsubALTlem4  20420  tsmsf1o  20517  ucnimalem  20653  ressxms  20898  uniretop  21139  cnfldtopn  21159  xrtgioo  21181  zcld  21188  icccmp  21200  xrge0gsumle  21208  xrge0tsms  21209  metnrmlem3  21235  fsum2cn  21245  cnmpt2pc  21298  oprpiece1res1  21321  oprpiece1res2  21322  evth  21329  evth2  21330  om1opn  21406  pi1xfrf  21423  pi1xfrcnv  21427  pi1cof  21429  clsocv  21560  cncmet  21631  cnflduss  21666  rrxprds  21691  ehlbase  21708  ismbl  21807  shftmbl  21819  ioorinv  21855  itg1addlem4  21976  itg2cnlem1  22038  iblitg  22045  itg0  22056  itgss3  22091  ditgneg  22131  limcdif  22150  limciun  22168  dvexp  22226  dvef  22251  dvcnvrelem2  22289  ftc1  22313  mdegfvalOLD  22331  plyremlem  22569  aannenlem2  22594  taylply2  22632  dvradcnv  22685  pserdvlem2  22692  reefgim  22714  cospi  22734  sincos6thpi  22777  tanregt0  22795  dflog2  22817  logfac  22854  dvlog  22901  cxpexp  22918  cxpmul2  22939  cxpsqrt  22953  dvsqrt  22987  cxpcn2  22989  ang180lem2  23011  isosctrlem2  23022  1cubrlem  23041  1cubr  23042  quart1lem  23055  atancj  23110  atanlogaddlem  23113  atansopn  23132  leibpilem2  23141  log2cnv  23144  log2ublem3  23148  birthdaylem1  23150  birthdaylem2  23151  birthday  23153  dfarea  23159  wilthlem2  23212  ftalem3  23217  ftalem7  23221  basellem2  23224  ppiprm  23294  ppinprm  23295  chtprm  23296  chtnprm  23297  ppi2  23313  ppi3  23314  ppiub  23348  chtub  23356  bclbnd  23424  bposlem8  23435  lgsdilem  23466  lgsdir2lem1  23467  lgsdir2lem2  23468  lgsdir2lem3  23469  lgsquadlem2  23499  lgsquad2lem2  23503  rplogsum  23581  mulog2sumlem2  23589  pnt2  23667  istrkg2ld  23727  axsegconlem9  24097  ax5seglem7  24107  usgrares1  24279  cusgrares  24341  wwlknprop  24555  wwlknfi  24607  wlknwwlknvbij  24609  clwwlkvbij  24670  eupath2lem3  24848  konigsberg  24856  ex-pw  25019  ex-xp  25026  ex-rn  25030  ablosn  25218  efghgrpOLD  25244  nvvop  25371  nvm  25405  cnims  25472  ip0i  25609  ip1ilem  25610  ipdirilem  25613  ipasslem10  25623  h2hva  25760  h2hsm  25761  h2hvs  25763  axhfvadd-zf  25768  axhvcom-zf  25769  axhvass-zf  25770  axhv0cl-zf  25771  axhvaddid-zf  25772  axhfvmul-zf  25773  axhvmulid-zf  25774  axhvmulass-zf  25775  axhvdistr1-zf  25776  axhvdistr2-zf  25777  axhvmul0-zf  25778  axhfi-zf  25779  axhis1-zf  25780  axhis2-zf  25781  axhis3-zf  25782  axhis4-zf  25783  axhcompl-zf  25784  normlem0  25895  normlem1  25896  normlem2  25897  normlem4  25899  normlem9  25904  bcseqi  25906  dfhnorm2  25908  norm3difi  25933  normpari  25940  normpar2i  25942  polid2i  25943  polidi  25944  hhba  25953  hhims  25958  hhims2  25959  hhsssh  26054  hhssims  26060  hhssims2  26061  shsval3i  26175  dfch2  26194  cmcm2i  26380  fh2  26406  qlaxr3i  26423  spansnji  26433  pjcji  26471  ho0val  26538  df0op2  26540  hosd1i  26610  hosd2i  26611  eigorthi  26625  hhlnoi  26688  hhnmoi  26689  hhbloi  26690  bra0  26738  nmop0  26774  nmfn0  26775  lnopeq0lem1  26793  lnopunilem1  26798  lnophmlem2  26805  nmopcoadji  26889  pjhmopidm  26971  cvmdi  27112  cdj3lem3  27226  cdj3lem3b  27228  abrexdomjm  27274  iundifdifd  27298  iundifdif  27299  mpt2mptxf  27387  df1stres  27391  df2ndres  27392  fcobijfs  27418  resf1o  27422  fpwrelmapffslem  27424  xrslt  27534  xrsclat  27538  gsumle  27640  xrge0tsmsd  27645  xrge0slmod  27704  fimaproj  27706  circtopn  27710  tpr2rico  27764  xrge0mulc1cn  27793  lmxrge0  27804  esumpfinvallem  27950  esumcocn  27956  hasheuni  27961  esumcvg  27962  measinblem  28061  aean  28086  sxbrsigalem3  28113  dya2iocival  28114  dya2iocucvr  28125  sxbrsigalem1  28126  sxbrsigalem2  28127  sxbrsigalem5  28129  sxbrsiga  28131  eulerpartlem1  28176  eulerpartgbij  28181  fibp1  28210  coinfliplem  28287  coinflipprob  28288  ballotlemfval  28298  ballotth  28346  sgnneg  28349  ofs2  28371  plymulx  28375  lgamgulmlem5  28445  lgambdd  28449  derang0  28483  subfacp1lem1  28493  subfacp1lem6  28499  kur14lem7  28526  cvmsss2  28589  cvmliftlem8  28607  cvmliftlem10  28609  msubfval  28754  quad3  28894  ghomgrpilem2  28896  fprod2d  29083  faclim  29143  predidm  29240  tz6.26  29257  dftrpred2  29274  bdayfo  29407  pprodcnveq  29505  dfon4  29515  fobigcup  29522  dfiota3  29545  dfrdg4  29572  dfint3  29574  bpoly2  29791  bpoly3  29792  bpoly4  29793  rankeq1o  29800  ssoninhaus  29885  onint1  29886  rabiun  30008  ptrest  30020  cnambfre  30035  ftc1anclem8  30069  dvcnsqrt  30073  refssfne  30148  fnopabco  30185  abrexdom  30193  cncfres  30233  scottexf  30548  scott0f  30549  mapfzcons  30620  eldioph4b  30717  diophren  30719  pwssplit4  31007  pwfi2f1o  31016  frlmpwfi  31018  mendplusgfval  31107  mendmulrfval  31109  mendvscafval  31112  idomodle  31126  cytpval  31142  arearect  31156  nznngen  31194  hashnzfz2  31199  lhe4.4ex1a  31207  compne  31300  refsum2cnlem1  31363  rnmptc  31399  iccdifprioo  31492  lptre2pt  31554  limclner  31565  stoweidlem13  31684  stoweidlem32  31703  stoweidlem62  31733  wallispi2lem2  31743  stirlinglem14  31758  dirkertrigeqlem1  31769  dirkercncflem4  31777  fourierdlem42  31820  fourierdlem73  31851  fourierdlem81  31859  fourierdlem92  31870  fourierdlem103  31881  fourierdlem104  31882  fouriercnp  31898  fouriersw  31903  rnfdmpr  32146  cznabel  32469  cznrng  32470  mpt2mptx2  32652  bnj1400  33622  bnj66  33646  bnj882  33712  bj-rababwv  34176  cdleme3d  35679  cdleme7a  35691  cdleme31sdnN  35836  cdlemk45  36396  inductionexd  37620
  Copyright terms: Public domain W3C validator