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

Theorem eqtr4i 2461
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 2442 . 2  |-  B  =  C
41, 3eqtri 2458 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431
This theorem is referenced by:  3eqtr2i  2464  3eqtr2ri  2465  3eqtr4i  2468  3eqtr4ri  2469  rabab  2985  cbvralcsf  3314  cbvrabcsf  3317  dfin5  3331  dfdif2  3332  uneqin  3596  unrab  3616  inrab  3617  inrab2  3618  difrab  3619  dfrab3ss  3623  rabun2  3624  rabxm  3655  difidALT  3743  difdifdir  3761  dfif3  3798  dfif5  3800  rabsnif  3939  tpidm  3974  ssunpr  4030  sstp  4032  dfint2  4125  iunrab  4212  uniiun  4218  intiin  4219  0iin  4223  mptv  4379  dfepfr  4700  epfrc  4701  xpundi  4886  xpundir  4887  csbcnv  5018  resiun2  5125  resopab  5148  opabresid  5154  dffr3  5196  dfse2  5197  cnvun  5237  imaundir  5245  imainrect  5274  cnvcnv2  5286  cnvcnvres  5297  dmtpop  5310  rnsnopg  5313  rnco2  5340  dmco  5341  co01  5347  unidmrn  5362  dfdm2  5364  dfmpt3  5528  mptun  5536  funcocnv2  5660  dffv2  5759  fnasrn  5883  fpr  5885  fmptap  5896  riotav  6052  dmoprab  6166  rnoprab2  6169  mpt2v  6175  mpt2mptx  6176  abrexex2g  6549  abrexex2  6553  1stval2  6589  2ndval2  6590  fo1st  6591  fo2nd  6592  xp2  6606  dfoprab4f  6627  offval22  6647  fmpt2co  6651  tposmpt2  6777  tposconst  6778  recsfval  6832  rdgsucmpt2  6878  frsucmpt2  6887  df2o3  6925  o1p1e2  6972  oarec  6993  omopthlem2  7087  ecqs  7156  qliftf  7180  erovlem  7188  mapsnf1o3  7253  ixp0x  7283  omf1o  7406  xpf1o  7465  mapunen  7472  enp1ilem  7538  pwfi  7598  marypha1lem  7675  marypha2lem4  7680  dfoi  7717  infeq5i  7834  oemapso  7882  cantnflem1  7889  cantnflem1OLD  7912  rankelop  8073  leweon  8170  r0weon  8171  kmlem11  8321  infcda1  8354  ackbij1lem16  8396  cf0  8412  cfsmolem  8431  alephsuc3  8736  fpwwe  8805  canthp1lem1  8811  wuncval2  8906  prlem936  9208  m1p1sr  9251  m1m1sr  9252  dfcnqs  9301  ssxr  9436  mul02lem2  9538  addid1  9541  3m1e2  10430  2p2e4  10431  3p2e5  10446  3p3e6  10447  4p2e6  10448  4p3e7  10449  4p4e8  10450  5p2e7  10451  5p3e8  10452  5p4e9  10453  5p5e10  10454  6p2e8  10455  6p3e9  10456  6p4e10  10457  7p2e9  10458  7p3e10  10459  8p2e10  10460  nn0suppOLD  10626  nnzrab  10666  nn0zrab  10667  dec0u  10762  dec0h  10763  decsuc  10770  decsucc  10774  numma  10778  decma  10785  decmac  10786  decma2c  10787  decadd  10788  decaddc  10789  decmul1c  10794  decmul2c  10795  5t5e25  10823  6t6e36  10828  8t6e48  10839  nn0uz  10887  nnuz  10888  xaddcom  11200  x2times  11254  ioomax  11362  iccmax  11363  ioopos  11364  ioorp  11365  prunioo  11406  fseq1p1m1  11526  fzo0to2pr  11606  fzo0to3tp  11607  om2uzrdg  11771  fzennn  11782  irec  11957  binom2aiOLD  11968  facnn  12045  fac0  12046  faclbnd2  12059  faclbnd4lem1  12061  hashfun  12191  hashbclem  12197  hashf1lem1  12200  hashf1lem2  12201  fz1isolem  12206  swrdccatin1  12366  swrdccat3blem  12378  s1co  12453  s2eq2s1eq  12535  fsumrev2  13241  fsumparts  13261  fsumiun  13276  isumnn0nn  13297  harmonic  13313  0.999...  13333  ege2le3  13367  cos1bnd  13463  efieq1re  13475  eirrlem  13478  qnnen  13488  cpnnen  13503  ruclem6  13509  3dvds  13588  m1bits  13628  algrp1  13741  phiprmpw  13843  prmreclem4  13972  4sqlem11  14008  4sqlem19  14016  dec5dvds  14085  decsplit1  14103  5prm  14128  7prm  14130  1259lem2  14148  1259lem3  14149  1259lem4  14150  1259lem5  14151  1259prm  14152  2503lem1  14153  2503lem2  14154  2503lem3  14155  2503prm  14156  4001lem1  14157  4001lem2  14158  4001lem3  14159  4001lem4  14160  4001prm  14161  ndxid  14187  strle1  14261  grpbasex  14273  grpplusgx  14274  divslem  14473  xpslem  14503  acsfn1  14591  acsfn2  14593  comfffval2  14632  xpchomfval  14981  xpccofval  14984  1stfval  14993  2ndfval  14996  oduleg  15294  ismgmid  15427  grpinvfvi  15570  gaorb  15816  cntri  15839  cntrsubgnsg  15849  cntrnsg  15850  oppglem  15856  oppgcntr  15871  gsumwrev  15872  symgbas  15876  symgga  15902  cayleylem1  15908  psgnunilem2  15992  efgval2  16212  efgredlemc  16233  efgcpbllema  16242  frgpnabllem1  16342  gsumzaddlem  16399  gsumzaddlemOLD  16401  mgplem  16586  opprlem  16710  oppr0  16715  opprneg  16717  rlmscaf  17269  mplbas  17483  mplbasOLD  17485  mpladd  17501  mplmul  17502  mplvsca2  17505  ressmplbas2  17514  ltbwe  17534  evlslem4OLD  17570  evlslem4  17571  psr1bas2  17626  ply1bas  17631  ply1assa  17635  mplplusg  17654  mplmulr  17655  psr1plusg  17656  psr1vsca  17657  psr1mulr  17658  ply1plusg  17659  ply1vsca  17660  ply1mulr  17661  ply1mpl0  17690  ply1mpl1  17691  coe1mul  17704  xrsds  17836  gsumfsum  17859  zringunit  17894  zrngunit  17895  cnmsgngrp  17989  psgnfix2  18009  relt  18025  ocv0  18082  thlle  18102  thlleval  18103  dsmmval2  18141  frlmip  18183  smadiadetglem1  18457  indistpsx  18594  iuncld  18629  tgrest  18743  resstopn  18770  leordtval2  18796  xkouni  19152  ptclsg  19168  ptuncnv  19360  ptunhmeo  19361  alexsubALTlem4  19602  tsmsf1o  19699  ucnimalem  19835  ressxms  20080  uniretop  20321  cnfldtopn  20341  xrtgioo  20363  zcld  20370  icccmp  20382  xrge0gsumle  20390  xrge0tsms  20391  metnrmlem3  20417  fsum2cn  20427  cnmpt2pc  20480  oprpiece1res1  20503  oprpiece1res2  20504  evth  20511  evth2  20512  om1opn  20588  pi1xfrf  20605  pi1xfrcnv  20609  pi1cof  20611  clsocv  20742  cncmet  20813  cnflduss  20848  rrxprds  20873  ehlbase  20890  ismbl  20989  shftmbl  21000  ioorinv  21036  itg1addlem4  21157  itg2cnlem1  21219  iblitg  21226  itg0  21237  itgss3  21272  ditgneg  21312  limcdif  21331  limciun  21349  dvexp  21407  dvef  21432  dvcnvrelem2  21470  ftc1  21494  mdegfvalOLD  21512  plyremlem  21750  aannenlem2  21775  taylply2  21813  dvradcnv  21866  pserdvlem2  21873  reefgim  21895  cospi  21914  sincos6thpi  21957  tanregt0  21975  dflog2  21992  logfac  22029  dvlog  22076  cxpexp  22093  cxpmul2  22114  cxpsqr  22128  dvsqr  22162  cxpcn2  22164  ang180lem2  22186  isosctrlem2  22197  1cubrlem  22216  1cubr  22217  quart1lem  22230  atancj  22285  atanlogaddlem  22288  atansopn  22307  leibpilem2  22316  log2cnv  22319  log2ublem3  22323  birthdaylem1  22325  birthdaylem2  22326  birthday  22328  dfarea  22334  wilthlem2  22387  ftalem3  22392  ftalem7  22396  basellem2  22399  ppiprm  22469  ppinprm  22470  chtprm  22471  chtnprm  22472  ppi2  22488  ppi3  22489  ppiub  22523  chtub  22531  bclbnd  22599  bposlem8  22610  lgsdilem  22641  lgsdir2lem1  22642  lgsdir2lem2  22643  lgsdir2lem3  22644  lgsquadlem2  22674  lgsquad2lem2  22678  rplogsum  22756  mulog2sumlem2  22764  pnt2  22842  axsegconlem9  23139  ax5seglem7  23149  usgrares1  23291  cusgrares  23348  eupath2lem3  23568  konigsberg  23576  ex-pw  23604  ex-xp  23611  ex-rn  23615  ablosn  23802  efghgrp  23828  nvvop  23955  nvm  23989  cnims  24056  ip0i  24193  ip1ilem  24194  ipdirilem  24197  ipasslem10  24207  h2hva  24344  h2hsm  24345  h2hvs  24347  axhfvadd-zf  24352  axhvcom-zf  24353  axhvass-zf  24354  axhv0cl-zf  24355  axhvaddid-zf  24356  axhfvmul-zf  24357  axhvmulid-zf  24358  axhvmulass-zf  24359  axhvdistr1-zf  24360  axhvdistr2-zf  24361  axhvmul0-zf  24362  axhfi-zf  24363  axhis1-zf  24364  axhis2-zf  24365  axhis3-zf  24366  axhis4-zf  24367  axhcompl-zf  24368  normlem0  24479  normlem1  24480  normlem2  24481  normlem4  24483  normlem9  24488  bcseqi  24490  dfhnorm2  24492  norm3difi  24517  normpari  24524  normpar2i  24526  polid2i  24527  polidi  24528  hhba  24537  hhims  24542  hhims2  24543  hhsssh  24638  hhssims  24644  hhssims2  24645  shsval3i  24759  dfch2  24778  cmcm2i  24964  fh2  24990  qlaxr3i  25007  spansnji  25017  pjcji  25055  ho0val  25122  df0op2  25124  hosd1i  25194  hosd2i  25195  eigorthi  25209  hhlnoi  25272  hhnmoi  25273  hhbloi  25274  bra0  25322  nmop0  25358  nmfn0  25359  lnopeq0lem1  25377  lnopunilem1  25382  lnophmlem2  25389  nmopcoadji  25473  pjhmopidm  25555  cvmdi  25696  cdj3lem3  25810  cdj3lem3b  25812  abrexdomjm  25856  iundifdifd  25880  iundifdif  25881  mpt2mptxf  25963  df1stres  25967  df2ndres  25968  fcobijfs  25994  resf1o  25998  fpwrelmapffslem  26000  xrslt  26105  xrsclat  26109  gsumle  26214  xrge0tsmsd  26221  xrge0slmod  26281  tpr2rico  26311  xrge0mulc1cn  26340  lmxrge0  26351  esumpfinvallem  26492  esumcocn  26498  hasheuni  26503  esumcvg  26504  measinblem  26603  ddemeas  26621  aean  26629  sxbrsigalem3  26656  dya2iocival  26657  dya2iocucvr  26668  sxbrsigalem1  26669  sxbrsigalem2  26670  sxbrsigalem5  26672  sxbrsiga  26674  sitgclbn  26698  eulerpartlem1  26719  eulerpartgbij  26724  eulerpart  26734  fibp1  26753  coinfliplem  26830  coinflipprob  26831  ballotlemfval  26841  ballotth  26889  sgnneg  26892  ofs2  26914  plymulx  26918  lgamgulmlem5  26988  lgambdd  26992  derang0  27026  subfacp1lem1  27036  subfacp1lem6  27042  kur14lem7  27069  cvmsss2  27132  cvmliftlem8  27150  cvmliftlem10  27152  ghomgrpilem2  27274  fprod2d  27461  faclim  27521  dfpred3  27604  predidm  27618  tz6.26  27635  dftrpred2  27652  bdayfo  27785  pprodcnveq  27883  dfon4  27893  fobigcup  27900  dfiota3  27923  dfrdg4  27950  dfint3  27952  bpoly2  28169  bpoly3  28170  bpoly4  28171  rankeq1o  28178  ssoninhaus  28264  onint1  28265  rabiun  28383  ptrest  28396  cnambfre  28411  ftc1anclem8  28445  dvcnsqr  28449  refssfne  28537  fnopabco  28587  abrexdom  28595  cncfres  28635  scottexf  28951  scott0f  28952  mapfzcons  29023  eldioph4b  29121  diophren  29123  pwssplit4  29413  pwfi2f1o  29422  frlmpwfi  29424  mendplusgfval  29513  mendmulrfval  29515  mendvscafval  29518  idomodle  29532  cytpval  29548  arearect  29562  lhe4.4ex1a  29574  compne  29667  refsum2cnlem1  29730  stoweidlem13  29779  stoweidlem32  29798  stoweidlem62  29828  wallispi2lem2  29838  stirlinglem14  29853  rnfdmpr  30120  wwlknprop  30291  wwlknfi  30341  wlknwwlknvbij  30343  clwwlkvbij  30434  mpt2mptx2  30694  matgsum  30822  bnj1400  31758  bnj66  31782  bnj882  31848  bj-rababwv  32278  cdleme3d  33768  cdleme7a  33780  cdleme31sdnN  33924  cdlemk45  34484
  Copyright terms: Public domain W3C validator