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

Theorem eqtr4i 2499
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 2480 . 2  |-  B  =  C
41, 3eqtri 2496 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  3eqtr2i  2502  3eqtr2ri  2503  3eqtr4i  2506  3eqtr4ri  2507  rabab  3131  cbvralcsf  3467  cbvrabcsf  3470  dfin5  3484  dfdif2  3485  uneqin  3749  unrab  3769  inrab  3770  inrab2  3771  difrab  3772  dfrab3ss  3776  rabun2  3777  rabxm  3808  difidALT  3896  difdifdir  3914  dfif3  3953  dfif5  3955  rabsnif  4096  tpidm  4131  ssunpr  4189  sstp  4191  dfint2  4284  iunrab  4372  uniiun  4378  intiin  4379  0iin  4383  mptv  4539  dfepfr  4864  epfrc  4865  xpundi  5051  xpundir  5052  csbcnv  5184  resiun2  5291  resopab  5318  opabresid  5325  dffr3  5367  dfse2  5368  cnvun  5409  imaundir  5417  imainrect  5446  cnvcnv2  5458  cnvcnvres  5469  dmtpop  5482  rnsnopg  5485  rnco2  5512  dmco  5513  co01  5520  unidmrn  5535  dfdm2  5537  dfmpt3  5701  mptun  5710  funcocnv2  5838  dffv2  5938  fnasrn  6065  fpr  6067  fmptap  6082  riotav  6248  dmoprab  6365  rnoprab2  6368  mpt2v  6374  mpt2mptx  6375  abrexex2g  6758  abrexex2  6762  1stval2  6798  2ndval2  6799  fo1st  6801  fo2nd  6802  xp2  6816  dfoprab4f  6839  offval22  6859  fmpt2co  6863  tposmpt2  6989  tposconst  6990  recsfval  7047  rdgsucmpt2  7093  frsucmpt2  7102  df2o3  7140  o1p1e2  7187  oarec  7208  omopthlem2  7302  ecqs  7372  qliftf  7396  erovlem  7404  mapsnf1o3  7464  ixp0x  7494  omf1o  7617  xpf1o  7676  mapunen  7683  enp1ilem  7750  pwfi  7811  marypha1lem  7889  marypha2lem4  7894  dfoi  7932  infeq5i  8049  oemapso  8097  cantnflem1  8104  cantnflem1OLD  8127  rankelop  8288  leweon  8385  r0weon  8386  kmlem11  8536  infcda1  8569  ackbij1lem16  8611  cf0  8627  cfsmolem  8646  alephsuc3  8951  fpwwe  9020  canthp1lem1  9026  wuncval2  9121  prlem936  9421  m1p1sr  9465  m1m1sr  9466  dfcnqs  9515  ssxr  9650  mul02lem2  9752  addid1  9755  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  10987  dec0h  10988  decsuc  10995  decsucc  10999  numma  11003  decma  11010  decmac  11011  decma2c  11012  decadd  11013  decaddc  11014  decmul1c  11019  decmul2c  11020  5t5e25  11048  6t6e36  11053  8t6e48  11064  nn0uz  11112  nnuz  11113  xaddcom  11433  x2times  11487  ioomax  11595  iccmax  11596  ioopos  11597  ioorp  11598  prunioo  11645  fseq1p1m1  11748  fzo0to2pr  11863  fzo0to3tp  11864  om2uzrdg  12031  fzennn  12042  irec  12231  binom2aiOLD  12242  facnn  12319  fac0  12320  faclbnd2  12333  faclbnd4lem1  12335  hashfun  12457  hashbclem  12463  hashf1lem1  12466  hashf1lem2  12467  fz1isolem  12472  swrdccatin1  12667  swrdccat3blem  12679  s1co  12758  s2eq2s1eq  12840  fsumrev2  13556  fsumparts  13579  fsumiun  13594  isumnn0nn  13613  harmonic  13629  0.999...  13649  ege2le3  13683  cos1bnd  13779  efieq1re  13791  eirrlem  13794  qnnen  13804  cpnnen  13819  ruclem6  13825  3dvds  13905  m1bits  13945  algrp1  14058  phiprmpw  14161  prmreclem4  14292  4sqlem11  14328  4sqlem19  14336  dec5dvds  14405  decsplit1  14423  5prm  14448  7prm  14450  1259lem2  14468  1259lem3  14469  1259lem4  14470  1259lem5  14471  1259prm  14472  2503lem1  14473  2503lem2  14474  2503lem3  14475  2503prm  14476  4001lem1  14477  4001lem2  14478  4001lem3  14479  4001lem4  14480  4001prm  14481  ndxid  14507  strle1  14582  grpbasex  14594  grpplusgx  14595  divslem  14794  xpslem  14824  acsfn1  14912  acsfn2  14914  comfffval2  14953  xpchomfval  15302  xpccofval  15305  1stfval  15314  2ndfval  15317  oduleg  15615  ismgmid  15748  grpinvfvi  15892  gaorb  16140  cntri  16163  cntrsubgnsg  16173  cntrnsg  16174  oppglem  16180  oppgcntr  16195  gsumwrev  16196  symgbas  16200  symgga  16226  cayleylem1  16232  psgnunilem2  16316  efgval2  16538  efgredlemc  16559  efgcpbllema  16568  frgpnabllem1  16668  gsumzaddlem  16725  gsumzaddlemOLD  16727  mgplem  16936  opprlem  17061  oppr0  17066  opprneg  17068  rlmscaf  17637  mplbas  17857  mplbasOLD  17859  mpladd  17875  mplmul  17876  mplvsca2  17879  ressmplbas2  17888  ltbwe  17908  evlslem4OLD  17944  evlslem4  17945  psr1bas2  18000  ply1bas  18005  ply1assa  18009  mplplusg  18032  mplmulr  18033  psr1plusg  18034  psr1vsca  18035  psr1mulr  18036  ply1plusg  18037  ply1vsca  18038  ply1mulr  18039  ply1mpl0  18067  ply1mpl1  18069  coe1mul  18082  xrsds  18229  gsumfsum  18252  zringunit  18287  zrngunit  18288  cnmsgngrp  18382  psgnfix2  18402  relt  18418  ocv0  18475  thlle  18495  thlleval  18496  dsmmval2  18534  frlmip  18576  matgsum  18706  smadiadetglem1  18940  indistpsx  19277  iuncld  19312  tgrest  19426  resstopn  19453  leordtval2  19479  xkouni  19835  ptclsg  19851  ptuncnv  20043  ptunhmeo  20044  alexsubALTlem4  20285  tsmsf1o  20382  ucnimalem  20518  ressxms  20763  uniretop  21004  cnfldtopn  21024  xrtgioo  21046  zcld  21053  icccmp  21065  xrge0gsumle  21073  xrge0tsms  21074  metnrmlem3  21100  fsum2cn  21110  cnmpt2pc  21163  oprpiece1res1  21186  oprpiece1res2  21187  evth  21194  evth2  21195  om1opn  21271  pi1xfrf  21288  pi1xfrcnv  21292  pi1cof  21294  clsocv  21425  cncmet  21496  cnflduss  21531  rrxprds  21556  ehlbase  21573  ismbl  21672  shftmbl  21684  ioorinv  21720  itg1addlem4  21841  itg2cnlem1  21903  iblitg  21910  itg0  21921  itgss3  21956  ditgneg  21996  limcdif  22015  limciun  22033  dvexp  22091  dvef  22116  dvcnvrelem2  22154  ftc1  22178  mdegfvalOLD  22196  plyremlem  22434  aannenlem2  22459  taylply2  22497  dvradcnv  22550  pserdvlem2  22557  reefgim  22579  cospi  22598  sincos6thpi  22641  tanregt0  22659  dflog2  22676  logfac  22713  dvlog  22760  cxpexp  22777  cxpmul2  22798  cxpsqrt  22812  dvsqrt  22846  cxpcn2  22848  ang180lem2  22870  isosctrlem2  22881  1cubrlem  22900  1cubr  22901  quart1lem  22914  atancj  22969  atanlogaddlem  22972  atansopn  22991  leibpilem2  23000  log2cnv  23003  log2ublem3  23007  birthdaylem1  23009  birthdaylem2  23010  birthday  23012  dfarea  23018  wilthlem2  23071  ftalem3  23076  ftalem7  23080  basellem2  23083  ppiprm  23153  ppinprm  23154  chtprm  23155  chtnprm  23156  ppi2  23172  ppi3  23173  ppiub  23207  chtub  23215  bclbnd  23283  bposlem8  23294  lgsdilem  23325  lgsdir2lem1  23326  lgsdir2lem2  23327  lgsdir2lem3  23328  lgsquadlem2  23358  lgsquad2lem2  23362  rplogsum  23440  mulog2sumlem2  23448  pnt2  23526  istrkg2ld  23586  axsegconlem9  23904  ax5seglem7  23914  usgrares1  24086  cusgrares  24148  wwlknprop  24362  wwlknfi  24414  wlknwwlknvbij  24416  clwwlkvbij  24477  eupath2lem3  24655  konigsberg  24663  ex-pw  24827  ex-xp  24834  ex-rn  24838  ablosn  25025  efghgrp  25051  nvvop  25178  nvm  25212  cnims  25279  ip0i  25416  ip1ilem  25417  ipdirilem  25420  ipasslem10  25430  h2hva  25567  h2hsm  25568  h2hvs  25570  axhfvadd-zf  25575  axhvcom-zf  25576  axhvass-zf  25577  axhv0cl-zf  25578  axhvaddid-zf  25579  axhfvmul-zf  25580  axhvmulid-zf  25581  axhvmulass-zf  25582  axhvdistr1-zf  25583  axhvdistr2-zf  25584  axhvmul0-zf  25585  axhfi-zf  25586  axhis1-zf  25587  axhis2-zf  25588  axhis3-zf  25589  axhis4-zf  25590  axhcompl-zf  25591  normlem0  25702  normlem1  25703  normlem2  25704  normlem4  25706  normlem9  25711  bcseqi  25713  dfhnorm2  25715  norm3difi  25740  normpari  25747  normpar2i  25749  polid2i  25750  polidi  25751  hhba  25760  hhims  25765  hhims2  25766  hhsssh  25861  hhssims  25867  hhssims2  25868  shsval3i  25982  dfch2  26001  cmcm2i  26187  fh2  26213  qlaxr3i  26230  spansnji  26240  pjcji  26278  ho0val  26345  df0op2  26347  hosd1i  26417  hosd2i  26418  eigorthi  26432  hhlnoi  26495  hhnmoi  26496  hhbloi  26497  bra0  26545  nmop0  26581  nmfn0  26582  lnopeq0lem1  26600  lnopunilem1  26605  lnophmlem2  26612  nmopcoadji  26696  pjhmopidm  26778  cvmdi  26919  cdj3lem3  27033  cdj3lem3b  27035  abrexdomjm  27079  iundifdifd  27102  iundifdif  27103  mpt2mptxf  27190  df1stres  27194  df2ndres  27195  fcobijfs  27221  resf1o  27225  fpwrelmapffslem  27227  xrslt  27326  xrsclat  27330  gsumle  27433  xrge0tsmsd  27438  xrge0slmod  27497  fimaproj  27499  tpr2rico  27530  xrge0mulc1cn  27559  lmxrge0  27570  circtopn  27638  esumpfinvallem  27720  esumcocn  27726  hasheuni  27731  esumcvg  27732  measinblem  27831  ddemeas  27848  aean  27856  sxbrsigalem3  27883  dya2iocival  27884  dya2iocucvr  27895  sxbrsigalem1  27896  sxbrsigalem2  27897  sxbrsigalem5  27899  sxbrsiga  27901  sitgclbn  27925  eulerpartlem1  27946  eulerpartgbij  27951  eulerpart  27961  fibp1  27980  coinfliplem  28057  coinflipprob  28058  ballotlemfval  28068  ballotth  28116  sgnneg  28119  ofs2  28141  plymulx  28145  lgamgulmlem5  28215  lgambdd  28219  derang0  28253  subfacp1lem1  28263  subfacp1lem6  28269  kur14lem7  28296  cvmsss2  28359  cvmliftlem8  28377  cvmliftlem10  28379  ghomgrpilem2  28501  fprod2d  28688  faclim  28748  dfpred3  28831  predidm  28845  tz6.26  28862  dftrpred2  28879  bdayfo  29012  pprodcnveq  29110  dfon4  29120  fobigcup  29127  dfiota3  29150  dfrdg4  29177  dfint3  29179  bpoly2  29396  bpoly3  29397  bpoly4  29398  rankeq1o  29405  ssoninhaus  29490  onint1  29491  rabiun  29613  ptrest  29625  cnambfre  29640  ftc1anclem8  29674  dvcnsqrt  29678  refssfne  29766  fnopabco  29816  abrexdom  29824  cncfres  29864  scottexf  30180  scott0f  30181  mapfzcons  30252  eldioph4b  30349  diophren  30351  pwssplit4  30639  pwfi2f1o  30648  frlmpwfi  30650  mendplusgfval  30739  mendmulrfval  30741  mendvscafval  30744  idomodle  30758  cytpval  30774  arearect  30788  nznngen  30821  hashnzfz2  30826  lhe4.4ex1a  30834  compne  30927  refsum2cnlem1  30990  rnmptc  31027  iccdifprioo  31120  lptre2pt  31182  stoweidlem13  31313  stoweidlem32  31332  stoweidlem62  31362  wallispi2lem2  31372  stirlinglem14  31387  fourierdlem92  31499  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  rnfdmpr  31777  mpt2mptx2  31988  bnj1400  32973  bnj66  32997  bnj882  33063  bj-rababwv  33524  cdleme3d  35027  cdleme7a  35039  cdleme31sdnN  35183  cdlemk45  35743
  Copyright terms: Public domain W3C validator