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

Theorem eqtr4i 2483
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 2464 . 2  |-  B  =  C
41, 3eqtri 2480 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-cleq 2443
This theorem is referenced by:  3eqtr2i  2486  3eqtr2ri  2487  3eqtr4i  2490  3eqtr4ri  2491  rabab  3086  cbvralcsf  3417  cbvrabcsf  3420  dfin5  3434  dfdif2  3435  uneqin  3699  unrab  3719  inrab  3720  inrab2  3721  difrab  3722  dfrab3ss  3726  rabun2  3727  rabxm  3758  difidALT  3846  difdifdir  3864  dfif3  3901  dfif5  3903  rabsnif  4042  tpidm  4077  ssunpr  4133  sstp  4135  dfint2  4228  iunrab  4315  uniiun  4321  intiin  4322  0iin  4326  mptv  4482  dfepfr  4803  epfrc  4804  xpundi  4989  xpundir  4990  csbcnv  5121  resiun2  5228  resopab  5251  opabresid  5257  dffr3  5299  dfse2  5300  cnvun  5340  imaundir  5348  imainrect  5377  cnvcnv2  5389  cnvcnvres  5400  dmtpop  5413  rnsnopg  5416  rnco2  5443  dmco  5444  co01  5450  unidmrn  5465  dfdm2  5467  dfmpt3  5631  mptun  5639  funcocnv2  5763  dffv2  5863  fnasrn  5987  fpr  5989  fmptap  6000  riotav  6156  dmoprab  6271  rnoprab2  6274  mpt2v  6280  mpt2mptx  6281  abrexex2g  6654  abrexex2  6658  1stval2  6694  2ndval2  6695  fo1st  6696  fo2nd  6697  xp2  6711  dfoprab4f  6732  offval22  6752  fmpt2co  6756  tposmpt2  6882  tposconst  6883  recsfval  6940  rdgsucmpt2  6986  frsucmpt2  6995  df2o3  7033  o1p1e2  7080  oarec  7101  omopthlem2  7195  ecqs  7264  qliftf  7288  erovlem  7296  mapsnf1o3  7361  ixp0x  7391  omf1o  7514  xpf1o  7573  mapunen  7580  enp1ilem  7647  pwfi  7707  marypha1lem  7784  marypha2lem4  7789  dfoi  7826  infeq5i  7943  oemapso  7991  cantnflem1  7998  cantnflem1OLD  8021  rankelop  8182  leweon  8279  r0weon  8280  kmlem11  8430  infcda1  8463  ackbij1lem16  8505  cf0  8521  cfsmolem  8540  alephsuc3  8845  fpwwe  8914  canthp1lem1  8920  wuncval2  9015  prlem936  9317  m1p1sr  9360  m1m1sr  9361  dfcnqs  9410  ssxr  9545  mul02lem2  9647  addid1  9650  3m1e2  10539  2p2e4  10540  3p2e5  10555  3p3e6  10556  4p2e6  10557  4p3e7  10558  4p4e8  10559  5p2e7  10560  5p3e8  10561  5p4e9  10562  5p5e10  10563  6p2e8  10564  6p3e9  10565  6p4e10  10566  7p2e9  10567  7p3e10  10568  8p2e10  10569  nn0suppOLD  10735  nnzrab  10775  nn0zrab  10776  dec0u  10871  dec0h  10872  decsuc  10879  decsucc  10883  numma  10887  decma  10894  decmac  10895  decma2c  10896  decadd  10897  decaddc  10898  decmul1c  10903  decmul2c  10904  5t5e25  10932  6t6e36  10937  8t6e48  10948  nn0uz  10996  nnuz  10997  xaddcom  11309  x2times  11363  ioomax  11471  iccmax  11472  ioopos  11473  ioorp  11474  prunioo  11515  fseq1p1m1  11635  fzo0to2pr  11715  fzo0to3tp  11716  om2uzrdg  11880  fzennn  11891  irec  12066  binom2aiOLD  12077  facnn  12154  fac0  12155  faclbnd2  12168  faclbnd4lem1  12170  hashfun  12301  hashbclem  12307  hashf1lem1  12310  hashf1lem2  12311  fz1isolem  12316  swrdccatin1  12476  swrdccat3blem  12488  s1co  12563  s2eq2s1eq  12645  fsumrev2  13351  fsumparts  13371  fsumiun  13386  isumnn0nn  13407  harmonic  13423  0.999...  13443  ege2le3  13477  cos1bnd  13573  efieq1re  13585  eirrlem  13588  qnnen  13598  cpnnen  13613  ruclem6  13619  3dvds  13698  m1bits  13738  algrp1  13851  phiprmpw  13953  prmreclem4  14082  4sqlem11  14118  4sqlem19  14126  dec5dvds  14195  decsplit1  14213  5prm  14238  7prm  14240  1259lem2  14258  1259lem3  14259  1259lem4  14260  1259lem5  14261  1259prm  14262  2503lem1  14263  2503lem2  14264  2503lem3  14265  2503prm  14266  4001lem1  14267  4001lem2  14268  4001lem3  14269  4001lem4  14270  4001prm  14271  ndxid  14297  strle1  14371  grpbasex  14383  grpplusgx  14384  divslem  14583  xpslem  14613  acsfn1  14701  acsfn2  14703  comfffval2  14742  xpchomfval  15091  xpccofval  15094  1stfval  15103  2ndfval  15106  oduleg  15404  ismgmid  15537  grpinvfvi  15681  gaorb  15927  cntri  15950  cntrsubgnsg  15960  cntrnsg  15961  oppglem  15967  oppgcntr  15982  gsumwrev  15983  symgbas  15987  symgga  16013  cayleylem1  16019  psgnunilem2  16103  efgval2  16325  efgredlemc  16346  efgcpbllema  16355  frgpnabllem1  16455  gsumzaddlem  16512  gsumzaddlemOLD  16514  mgplem  16701  opprlem  16826  oppr0  16831  opprneg  16833  rlmscaf  17395  mplbas  17610  mplbasOLD  17612  mpladd  17628  mplmul  17629  mplvsca2  17632  ressmplbas2  17641  ltbwe  17661  evlslem4OLD  17697  evlslem4  17698  psr1bas2  17753  ply1bas  17758  ply1assa  17762  mplplusg  17781  mplmulr  17782  psr1plusg  17783  psr1vsca  17784  psr1mulr  17785  ply1plusg  17786  ply1vsca  17787  ply1mulr  17788  ply1mpl0  17817  ply1mpl1  17818  coe1mul  17831  xrsds  17965  gsumfsum  17988  zringunit  18023  zrngunit  18024  cnmsgngrp  18118  psgnfix2  18138  relt  18154  ocv0  18211  thlle  18231  thlleval  18232  dsmmval2  18270  frlmip  18312  smadiadetglem1  18593  indistpsx  18730  iuncld  18765  tgrest  18879  resstopn  18906  leordtval2  18932  xkouni  19288  ptclsg  19304  ptuncnv  19496  ptunhmeo  19497  alexsubALTlem4  19738  tsmsf1o  19835  ucnimalem  19971  ressxms  20216  uniretop  20457  cnfldtopn  20477  xrtgioo  20499  zcld  20506  icccmp  20518  xrge0gsumle  20526  xrge0tsms  20527  metnrmlem3  20553  fsum2cn  20563  cnmpt2pc  20616  oprpiece1res1  20639  oprpiece1res2  20640  evth  20647  evth2  20648  om1opn  20724  pi1xfrf  20741  pi1xfrcnv  20745  pi1cof  20747  clsocv  20878  cncmet  20949  cnflduss  20984  rrxprds  21009  ehlbase  21026  ismbl  21125  shftmbl  21136  ioorinv  21172  itg1addlem4  21293  itg2cnlem1  21355  iblitg  21362  itg0  21373  itgss3  21408  ditgneg  21448  limcdif  21467  limciun  21485  dvexp  21543  dvef  21568  dvcnvrelem2  21606  ftc1  21630  mdegfvalOLD  21648  plyremlem  21886  aannenlem2  21911  taylply2  21949  dvradcnv  22002  pserdvlem2  22009  reefgim  22031  cospi  22050  sincos6thpi  22093  tanregt0  22111  dflog2  22128  logfac  22165  dvlog  22212  cxpexp  22229  cxpmul2  22250  cxpsqr  22264  dvsqr  22298  cxpcn2  22300  ang180lem2  22322  isosctrlem2  22333  1cubrlem  22352  1cubr  22353  quart1lem  22366  atancj  22421  atanlogaddlem  22424  atansopn  22443  leibpilem2  22452  log2cnv  22455  log2ublem3  22459  birthdaylem1  22461  birthdaylem2  22462  birthday  22464  dfarea  22470  wilthlem2  22523  ftalem3  22528  ftalem7  22532  basellem2  22535  ppiprm  22605  ppinprm  22606  chtprm  22607  chtnprm  22608  ppi2  22624  ppi3  22625  ppiub  22659  chtub  22667  bclbnd  22735  bposlem8  22746  lgsdilem  22777  lgsdir2lem1  22778  lgsdir2lem2  22779  lgsdir2lem3  22780  lgsquadlem2  22810  lgsquad2lem2  22814  rplogsum  22892  mulog2sumlem2  22900  pnt2  22978  istrkg2ld  23038  axsegconlem9  23306  ax5seglem7  23316  usgrares1  23458  cusgrares  23515  eupath2lem3  23735  konigsberg  23743  ex-pw  23771  ex-xp  23778  ex-rn  23782  ablosn  23969  efghgrp  23995  nvvop  24122  nvm  24156  cnims  24223  ip0i  24360  ip1ilem  24361  ipdirilem  24364  ipasslem10  24374  h2hva  24511  h2hsm  24512  h2hvs  24514  axhfvadd-zf  24519  axhvcom-zf  24520  axhvass-zf  24521  axhv0cl-zf  24522  axhvaddid-zf  24523  axhfvmul-zf  24524  axhvmulid-zf  24525  axhvmulass-zf  24526  axhvdistr1-zf  24527  axhvdistr2-zf  24528  axhvmul0-zf  24529  axhfi-zf  24530  axhis1-zf  24531  axhis2-zf  24532  axhis3-zf  24533  axhis4-zf  24534  axhcompl-zf  24535  normlem0  24646  normlem1  24647  normlem2  24648  normlem4  24650  normlem9  24655  bcseqi  24657  dfhnorm2  24659  norm3difi  24684  normpari  24691  normpar2i  24693  polid2i  24694  polidi  24695  hhba  24704  hhims  24709  hhims2  24710  hhsssh  24805  hhssims  24811  hhssims2  24812  shsval3i  24926  dfch2  24945  cmcm2i  25131  fh2  25157  qlaxr3i  25174  spansnji  25184  pjcji  25222  ho0val  25289  df0op2  25291  hosd1i  25361  hosd2i  25362  eigorthi  25376  hhlnoi  25439  hhnmoi  25440  hhbloi  25441  bra0  25489  nmop0  25525  nmfn0  25526  lnopeq0lem1  25544  lnopunilem1  25549  lnophmlem2  25556  nmopcoadji  25640  pjhmopidm  25722  cvmdi  25863  cdj3lem3  25977  cdj3lem3b  25979  abrexdomjm  26023  iundifdifd  26046  iundifdif  26047  mpt2mptxf  26129  df1stres  26133  df2ndres  26134  fcobijfs  26160  resf1o  26164  fpwrelmapffslem  26166  xrslt  26271  xrsclat  26275  gsumle  26380  xrge0tsmsd  26387  xrge0slmod  26446  tpr2rico  26476  xrge0mulc1cn  26505  lmxrge0  26516  esumpfinvallem  26657  esumcocn  26663  hasheuni  26668  esumcvg  26669  measinblem  26768  ddemeas  26786  aean  26794  sxbrsigalem3  26821  dya2iocival  26822  dya2iocucvr  26833  sxbrsigalem1  26834  sxbrsigalem2  26835  sxbrsigalem5  26837  sxbrsiga  26839  sitgclbn  26863  eulerpartlem1  26884  eulerpartgbij  26889  eulerpart  26899  fibp1  26918  coinfliplem  26995  coinflipprob  26996  ballotlemfval  27006  ballotth  27054  sgnneg  27057  ofs2  27079  plymulx  27083  lgamgulmlem5  27153  lgambdd  27157  derang0  27191  subfacp1lem1  27201  subfacp1lem6  27207  kur14lem7  27234  cvmsss2  27297  cvmliftlem8  27315  cvmliftlem10  27317  ghomgrpilem2  27439  fprod2d  27626  faclim  27686  dfpred3  27769  predidm  27783  tz6.26  27800  dftrpred2  27817  bdayfo  27950  pprodcnveq  28048  dfon4  28058  fobigcup  28065  dfiota3  28088  dfrdg4  28115  dfint3  28117  bpoly2  28334  bpoly3  28335  bpoly4  28336  rankeq1o  28343  ssoninhaus  28428  onint1  28429  rabiun  28550  ptrest  28563  cnambfre  28578  ftc1anclem8  28612  dvcnsqr  28616  refssfne  28704  fnopabco  28754  abrexdom  28762  cncfres  28802  scottexf  29118  scott0f  29119  mapfzcons  29190  eldioph4b  29288  diophren  29290  pwssplit4  29580  pwfi2f1o  29589  frlmpwfi  29591  mendplusgfval  29680  mendmulrfval  29682  mendvscafval  29685  idomodle  29699  cytpval  29715  arearect  29729  lhe4.4ex1a  29741  compne  29834  refsum2cnlem1  29897  stoweidlem13  29946  stoweidlem32  29965  stoweidlem62  29995  wallispi2lem2  30005  stirlinglem14  30020  rnfdmpr  30287  wwlknprop  30458  wwlknfi  30508  wlknwwlknvbij  30510  clwwlkvbij  30601  mpt2mptx2  30862  matgsum  31015  bnj1400  32129  bnj66  32153  bnj882  32219  bj-rababwv  32678  cdleme3d  34181  cdleme7a  34193  cdleme31sdnN  34337  cdlemk45  34897
  Copyright terms: Public domain W3C validator