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

Theorem eqtr4i 2452
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 2433 . 2  |-  B  =  C
41, 3eqtri 2449 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-cleq 2412
This theorem is referenced by:  3eqtr2i  2455  3eqtr2ri  2456  3eqtr4i  2459  3eqtr4ri  2460  rabab  3096  cbvralcsf  3424  cbvrabcsf  3427  dfin5  3441  dfdif2  3442  uneqin  3721  unrab  3741  inrab  3742  inrab2  3743  difrab  3744  dfrab3ss  3748  rabun2  3749  rabxm  3782  difidALT  3861  difdifdir  3880  dfif3  3920  dfif5  3922  rabsnif  4063  tpidm  4098  ssunpr  4156  sstp  4158  dfint2  4251  iunrab  4340  uniiun  4346  intiin  4347  0iin  4351  mptv  4510  dfepfr  4830  epfrc  4831  xpundi  4898  xpundir  4899  csbcnv  5029  resiun2  5135  resopab  5162  opabresid  5169  dffr3  5212  dfse2  5213  cnvun  5252  imaundir  5260  imainrect  5289  cnvcnv2  5300  cnvcnvres  5310  dmtpop  5323  rnsnopg  5326  rnco2  5353  dmco  5354  co01  5361  unidmrn  5377  dfdm2  5379  predidm  5412  tz6.26  5421  dfmpt3  5707  mptun  5718  funcocnv2  5846  dffv2  5945  fnasrn  6076  fpr  6078  fmptap  6093  riotav  6263  dmoprab  6382  rnoprab2  6385  mpt2v  6391  mpt2mptx  6392  abrexex2g  6775  abrexex2  6779  1stval2  6815  2ndval2  6816  fo1st  6818  fo2nd  6819  xp2  6833  dfoprab4f  6856  offval22  6877  fmpt2co  6881  tposmpt2  7009  tposconst  7010  recsfval  7098  rdgsucmpt2  7147  frsucmpt2  7156  df2o3  7194  o1p1e2  7241  oarec  7262  omopthlem2  7356  ecqs  7426  qliftf  7450  erovlem  7458  mapsnf1o3  7519  ixp0x  7549  omf1o  7672  xpf1o  7731  mapunen  7738  enp1ilem  7802  pwfi  7866  marypha1lem  7944  marypha2lem4  7949  dfoi  8017  infeq5i  8132  oemapso  8177  cantnflem1  8184  rankelop  8335  leweon  8432  r0weon  8433  kmlem11  8579  infcda1  8612  ackbij1lem16  8654  cf0  8670  cfsmolem  8689  alephsuc3  8994  fpwwe  9060  canthp1lem1  9066  wuncval2  9161  prlem936  9461  m1p1sr  9505  m1m1sr  9506  dfcnqs  9555  ssxr  9692  mul02lem2  9799  addid1  9802  3m1e2  10715  2p2e4  10716  3p2e5  10731  3p3e6  10732  4p2e6  10733  4p3e7  10734  4p4e8  10735  5p2e7  10736  5p3e8  10737  5p4e9  10738  5p5e10  10739  6p2e8  10740  6p3e9  10741  6p4e10  10742  7p2e9  10743  7p3e10  10744  8p2e10  10745  nnzrab  10954  nn0zrab  10955  dec0u  11055  dec0h  11056  decsuc  11063  decsucc  11067  numma  11071  decma  11078  decmac  11079  decma2c  11080  decadd  11081  decaddc  11082  decmul1c  11087  decmul2c  11088  5t5e25  11116  6t6e36  11121  8t6e48  11132  nn0uz  11182  nnuz  11183  xaddcom  11520  x2times  11574  ioomax  11698  iccmax  11699  ioopos  11700  ioorp  11701  prunioo  11748  fseq1p1m1  11855  fzo13pr  11983  fzo0to2pr  11984  fzo0to3tp  11985  om2uzrdg  12156  fzennn  12167  irec  12360  facnn  12447  fac0  12448  faclbnd2  12462  faclbnd4lem1  12464  hashfun  12593  hashbclem  12599  hashf1lem1  12602  hashf1lem2  12603  fz1isolem  12608  swrdccatin1  12813  swrdccat3blem  12825  s1co  12904  s2eq2s1eq  12986  dfid5  13058  dfid6  13059  fsumrev2  13810  fsumparts  13833  fsumiun  13848  isumnn0nn  13867  harmonic  13884  0.999...  13904  fprod2d  14002  bpoly2  14077  bpoly3  14078  bpoly4  14079  ege2le3  14111  cos1bnd  14208  efieq1re  14220  eirrlem  14223  qnnen  14233  cpnnen  14248  ruclem6  14254  3dvds  14336  m1bits  14377  algrp1  14493  phiprmpw  14682  prmreclem4  14815  4sqlem11  14851  4sqlem19  14865  dec5dvds  14988  decsplit1  15006  5prm  15032  7prm  15034  1259lem2  15055  1259lem3  15056  1259lem4  15057  1259lem5  15058  1259prm  15059  2503lem1  15060  2503lem2  15061  2503lem3  15062  2503prm  15063  4001lem1  15064  4001lem2  15065  4001lem3  15066  4001lem4  15067  4001prm  15068  ndxid  15094  strle1  15173  grpbasex  15192  grpplusgx  15193  quslem  15393  xpslem  15423  acsfn1  15511  acsfn2  15513  comfffval2  15550  xpchomfval  16008  xpccofval  16011  1stfval  16020  2ndfval  16023  oduleg  16322  ismgmid  16451  grpinvfvi  16651  gaorb  16905  cntri  16928  cntrsubgnsg  16938  cntrnsg  16939  oppglem  16945  oppgcntr  16960  gsumwrev  16961  symgbas  16965  symgga  16991  cayleylem1  16997  psgnunilem2  17080  efgval2  17302  efgredlemc  17323  efgcpbllema  17332  frgpnabllem1  17437  gsumzaddlem  17482  mgplem  17656  opprlem  17784  oppr0  17789  opprneg  17791  rlmscaf  18359  mplbas  18581  mpladd  18594  mplmul  18595  mplvsca2  18598  ressmplbas2  18607  ltbwe  18624  evlslem4  18659  psr1bas2  18711  ply1bas  18716  ply1assa  18720  mplplusg  18741  mplmulr  18742  psr1plusg  18743  psr1vsca  18744  psr1mulr  18745  ply1plusg  18746  ply1vsca  18747  ply1mulr  18748  ply1mpl0  18776  ply1mpl1  18778  coe1mul  18791  xrsds  18939  gsumfsum  18962  zringunit  18986  cnmsgngrp  19071  psgnfix2  19091  relt  19107  ocv0  19164  thlle  19184  thlleval  19185  dsmmval2  19223  frlmip  19260  matgsum  19386  smadiadetglem1  19620  indistpsx  19949  iuncld  19984  tgrest  20099  resstopn  20126  leordtval2  20152  xkouni  20538  ptclsg  20554  ptuncnv  20746  ptunhmeo  20747  alexsubALTlem4  20989  tsmsf1o  21083  ucnimalem  21219  ressxms  21464  uniretop  21687  cnfldtopn  21706  xrtgioo  21728  zcld  21735  icccmp  21747  xrge0gsumle  21755  xrge0tsms  21756  metnrmlem3  21782  fsum2cn  21792  cnmpt2pc  21845  oprpiece1res1  21868  oprpiece1res2  21869  evth  21876  evth2  21877  om1opn  21953  pi1xfrf  21970  pi1xfrcnv  21974  pi1cof  21976  clsocv  22107  cncmet  22176  cnflduss  22209  rrxprds  22234  ehlbase  22251  ismbl  22354  shftmbl  22366  ioorinv  22402  ioorinvOLD  22407  itg1addlem4  22531  itg2cnlem1  22593  iblitg  22600  itg0  22611  itgss3  22646  ditgneg  22686  limcdif  22705  limciun  22723  dvexp  22781  dvef  22806  dvcnvrelem2  22844  ftc1  22868  plyremlem  23122  aannenlem2  23147  taylply2  23185  dvradcnv  23238  pserdvlem2  23245  reefgim  23267  cospi  23289  sincos6thpi  23332  tanregt0  23350  dflog2  23372  logfac  23412  dvlog  23458  cxpexp  23475  cxpmul2  23496  cxpsqrt  23510  dvsqrt  23544  dvcnsqrt  23546  cxpcn2  23548  ang180lem2  23601  isosctrlem2  23610  1cubrlem  23629  1cubr  23630  quart1lem  23643  atancj  23698  atanlogaddlem  23701  atansopn  23720  leibpilem2  23729  log2cnv  23732  log2ublem3  23736  birthdaylem1  23739  birthdaylem2  23740  birthday  23742  dfarea  23748  lgamgulmlem5  23820  lgambdd  23824  wilthlem2  23856  ftalem3  23861  ftalem7  23865  basellem2  23868  ppiprm  23938  ppinprm  23939  chtprm  23940  chtnprm  23941  ppi2  23957  ppi3  23958  ppiub  23992  chtub  24000  bclbnd  24068  bposlem8  24079  lgsdilem  24110  lgsdir2lem1  24111  lgsdir2lem2  24112  lgsdir2lem3  24113  lgsquadlem2  24143  lgsquad2lem2  24147  rplogsum  24225  mulog2sumlem2  24233  pnt2  24311  istrkg2ld  24368  axsegconlem9  24798  ax5seglem7  24808  usgrares1  24980  cusgrares  25042  wwlknprop  25256  wwlknfi  25308  wlknwwlknvbij  25310  clwwlkvbij  25371  eupath2lem3  25549  konigsberg  25557  ex-pw  25721  ex-xp  25728  ex-rn  25732  ablosn  25917  efghgrpOLD  25943  nvvop  26070  nvm  26104  cnims  26171  ip0i  26308  ip1ilem  26309  ipdirilem  26312  ipasslem10  26322  h2hva  26459  h2hsm  26460  h2hvs  26462  axhfvadd-zf  26467  axhvcom-zf  26468  axhvass-zf  26469  axhv0cl-zf  26470  axhvaddid-zf  26471  axhfvmul-zf  26472  axhvmulid-zf  26473  axhvmulass-zf  26474  axhvdistr1-zf  26475  axhvdistr2-zf  26476  axhvmul0-zf  26477  axhfi-zf  26478  axhis1-zf  26479  axhis2-zf  26480  axhis3-zf  26481  axhis4-zf  26482  axhcompl-zf  26483  normlem0  26594  normlem1  26595  normlem2  26596  normlem4  26598  normlem9  26603  bcseqi  26605  dfhnorm2  26607  norm3difi  26632  normpari  26639  normpar2i  26641  polid2i  26642  polidi  26643  hhba  26652  hhims  26657  hhims2  26658  hhsssh  26752  hhssims  26758  hhssims2  26759  shsval3i  26873  dfch2  26892  cmcm2i  27078  fh2  27104  qlaxr3i  27121  spansnji  27131  pjcji  27169  ho0val  27235  df0op2  27237  hosd1i  27307  hosd2i  27308  eigorthi  27322  hhlnoi  27385  hhnmoi  27386  hhbloi  27387  bra0  27435  nmop0  27471  nmfn0  27472  lnopeq0lem1  27490  lnopunilem1  27495  lnophmlem2  27502  nmopcoadji  27586  pjhmopidm  27668  cvmdi  27809  cdj3lem3  27923  cdj3lem3b  27925  abrexdomjm  27974  uniin1  28000  uniin2  28001  iundifdifd  28013  iundifdif  28014  mpt2mptxf  28117  df1stres  28121  df2ndres  28122  fcobijfs  28151  resf1o  28155  fpwrelmapffslem  28157  xrslt  28272  xrsclat  28276  gsumle  28377  xrge0tsmsd  28384  xrge0slmod  28443  fimaproj  28496  circtopn  28500  tpr2rico  28554  xrge0mulc1cn  28583  lmxrge0  28594  esumpfinvallem  28731  esumcocn  28737  hasheuni  28742  esumcvg  28743  rossros  28838  measinblem  28878  aean  28903  sxbrsigalem3  28930  dya2iocival  28931  dya2iocucvr  28942  sxbrsigalem1  28943  sxbrsigalem2  28944  sxbrsigalem5  28946  sxbrsiga  28948  fiunelcarsg  28974  eulerpartlem1  29023  eulerpartgbij  29028  fibp1  29057  coinfliplem  29134  coinflipprob  29135  ballotlemfval  29145  ballotth  29193  sgnneg  29196  ofs2  29218  plymulx  29222  bnj1400  29432  bnj66  29456  bnj882  29522  derang0  29677  subfacp1lem1  29687  subfacp1lem6  29693  kur14lem7  29720  cvmsss2  29782  cvmliftlem8  29800  cvmliftlem10  29802  msubfval  29947  quad3  30087  ghomgrpilem2  30089  bcprod  30158  bccolsum  30159  faclim  30166  dftrpred2  30244  bdayfo  30346  pprodcnveq  30432  dfon4  30442  fobigcup  30449  dfiota3  30472  dfrecs2  30499  dfrdg4  30500  dfint3  30501  rankeq1o  30720  refssfne  30796  ssoninhaus  30890  onint1  30891  bj-rababwv  31224  bj-inrab3  31279  rnmptsn  31468  dissneq  31474  rabiun  31630  ptrest  31643  poimirlem3  31647  poimirlem4  31648  poimirlem13  31657  poimirlem16  31660  poimirlem22  31666  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem30  31674  cnambfre  31693  ftc1anclem8  31728  fnopabco  31753  abrexdom  31761  cncfres  31801  scottexf  32115  scott0f  32116  cdleme3d  33506  cdleme7a  33518  cdleme31sdnN  33663  cdlemk45  34223  mapfzcons  35267  eldioph4b  35363  diophren  35365  pwssplit4  35657  pwfi2f1o  35664  frlmpwfi  35666  mendplusgfval  35754  mendmulrfval  35756  mendvscafval  35759  idomodle  35773  cytpval  35789  arearect  35803  dfrcl3  35910  dfrcl4  35911  comptiunov2i  35941  corcltrcl  35974  inductionexd  36234  nznngen  36306  hashnzfz2  36311  lhe4.4ex1a  36319  dvradcnv2  36337  binomcxplemrat  36340  binomcxplemnotnn0  36346  compne  36434  refsum2cnlem1  37002  fiiuncl  37052  rnmptc  37063  iccdifprioo  37206  lptre2pt  37296  limclner  37308  stoweidlem13  37446  stoweidlem32  37466  stoweidlem62  37496  stoweidlem62OLD  37497  wallispi2lem2  37507  stirlinglem14  37522  dirkertrigeqlem1  37533  dirkercncflem4  37541  fourierdlem42  37584  fourierdlem73  37615  fourierdlem81  37623  fourierdlem92  37634  fourierdlem103  37645  fourierdlem104  37646  fouriercnp  37662  fouriersw  37667  sge0tsms  37760  sge0iunmptlemfi  37793  opoeALTV  38215  evengpop3  38296  rnfdmpr  38398  cznabel  38727  cznrng  38728  mpt2mptx2  38889
  Copyright terms: Public domain W3C validator