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

Theorem eqtr4i 2456
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-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 2437 . 2  |-  B  =  C
41, 3eqtri 2453 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  3eqtr2i  2459  3eqtr2ri  2460  3eqtr4i  2463  3eqtr4ri  2464  rabab  2980  cbvralcsf  3307  cbvrabcsf  3310  dfin5  3324  dfdif2  3325  uneqin  3589  unrab  3609  inrab  3610  inrab2  3611  difrab  3612  dfrab3ss  3616  rabun2  3617  rabxm  3648  difidALT  3736  difdifdir  3754  dfif3  3791  dfif5  3793  rabsnif  3932  tpidm  3967  ssunpr  4023  sstp  4025  dfint2  4118  iunrab  4205  uniiun  4211  intiin  4212  0iin  4216  mptv  4372  dfepfr  4692  epfrc  4693  xpundi  4878  xpundir  4879  csbcnv  5010  resiun2  5118  resopab  5141  opabresid  5147  dffr3  5189  dfse2  5190  cnvun  5230  imaundir  5238  imainrect  5267  cnvcnv2  5279  cnvcnvres  5290  dmtpop  5303  rnsnopg  5306  rnco2  5333  dmco  5334  co01  5340  unidmrn  5355  dfdm2  5357  dfmpt3  5521  mptun  5529  funcocnv2  5653  dffv2  5752  fnasrn  5875  fpr  5877  fmptap  5888  riotav  6044  dmoprab  6160  rnoprab2  6163  mpt2v  6169  mpt2mptx  6170  abrexex2g  6543  abrexex2  6547  1stval2  6583  2ndval2  6584  fo1st  6585  fo2nd  6586  xp2  6600  dfoprab4f  6621  offval22  6641  fmpt2co  6645  tposmpt2  6771  tposconst  6772  recsfval  6826  rdgsucmpt2  6872  frsucmpt2  6881  df2o3  6921  o1p1e2  6968  oarec  6989  omopthlem2  7083  ecqs  7152  qliftf  7176  erovlem  7184  mapsnf1o3  7249  ixp0x  7279  omf1o  7402  xpf1o  7461  mapunen  7468  enp1ilem  7534  pwfi  7594  marypha1lem  7671  marypha2lem4  7676  dfoi  7713  infeq5i  7830  oemapso  7878  cantnflem1  7885  cantnflem1OLD  7908  rankelop  8069  leweon  8166  r0weon  8167  kmlem11  8317  infcda1  8350  ackbij1lem16  8392  cf0  8408  cfsmolem  8427  alephsuc3  8732  fpwwe  8800  canthp1lem1  8806  wuncval2  8901  prlem936  9203  m1p1sr  9246  m1m1sr  9247  dfcnqs  9296  ssxr  9431  mul02lem2  9533  addid1  9536  3m1e2  10425  2p2e4  10426  3p2e5  10441  3p3e6  10442  4p2e6  10443  4p3e7  10444  4p4e8  10445  5p2e7  10446  5p3e8  10447  5p4e9  10448  5p5e10  10449  6p2e8  10450  6p3e9  10451  6p4e10  10452  7p2e9  10453  7p3e10  10454  8p2e10  10455  nn0suppOLD  10621  nnzrab  10661  nn0zrab  10662  dec0u  10757  dec0h  10758  decsuc  10765  decsucc  10769  numma  10773  decma  10780  decmac  10781  decma2c  10782  decadd  10783  decaddc  10784  decmul1c  10789  decmul2c  10790  5t5e25  10818  6t6e36  10823  8t6e48  10834  nn0uz  10882  nnuz  10883  xaddcom  11195  x2times  11249  ioomax  11357  iccmax  11358  ioopos  11359  ioorp  11360  prunioo  11400  fseq1p1m1  11517  fzo0to2pr  11597  fzo0to3tp  11598  om2uzrdg  11762  fzennn  11773  irec  11948  binom2aiOLD  11959  facnn  12036  fac0  12037  faclbnd2  12050  faclbnd4lem1  12052  hashfun  12182  hashbclem  12188  hashf1lem1  12191  hashf1lem2  12192  fz1isolem  12197  swrdccatin1  12357  swrdccat3blem  12369  s1co  12444  s2eq2s1eq  12526  fsumrev2  13231  fsumparts  13251  fsumiun  13266  isumnn0nn  13287  harmonic  13303  0.999...  13323  ege2le3  13357  cos1bnd  13453  efieq1re  13465  eirrlem  13468  qnnen  13478  cpnnen  13493  ruclem6  13499  3dvds  13578  m1bits  13618  algrp1  13731  phiprmpw  13833  prmreclem4  13962  4sqlem11  13998  4sqlem19  14006  dec5dvds  14075  decsplit1  14093  5prm  14118  7prm  14120  1259lem2  14138  1259lem3  14139  1259lem4  14140  1259lem5  14141  1259prm  14142  2503lem1  14143  2503lem2  14144  2503lem3  14145  2503prm  14146  4001lem1  14147  4001lem2  14148  4001lem3  14149  4001lem4  14150  4001prm  14151  ndxid  14177  strle1  14251  grpbasex  14263  grpplusgx  14264  divslem  14463  xpslem  14493  acsfn1  14581  acsfn2  14583  comfffval2  14622  xpchomfval  14971  xpccofval  14974  1stfval  14983  2ndfval  14986  oduleg  15284  ismgmid  15417  grpinvfvi  15558  gaorb  15804  cntri  15827  cntrsubgnsg  15837  cntrnsg  15838  oppglem  15844  oppgcntr  15859  gsumwrev  15860  symgbas  15864  symgga  15890  cayleylem1  15896  psgnunilem2  15980  efgval2  16200  efgredlemc  16221  efgcpbllema  16230  frgpnabllem1  16330  gsumzaddlem  16387  gsumzaddlemOLD  16389  mgplem  16569  opprlem  16653  oppr0  16658  opprneg  16660  rlmscaf  17210  mplbas  17436  mplbasOLD  17438  mpladd  17454  mplmul  17455  mplvsca2  17458  ressmplbas2  17467  ltbwe  17485  evlslem4OLD  17517  evlslem4  17518  psr1bas2  17544  ply1bas  17549  ply1assa  17553  mplplusg  17572  mplmulr  17573  psr1plusg  17574  psr1vsca  17575  psr1mulr  17576  ply1plusg  17577  ply1vsca  17578  ply1mulr  17579  ply1mpl0  17607  ply1mpl1  17608  coe1mul  17621  xrsds  17699  gsumfsum  17722  zringunit  17755  zrngunit  17756  cnmsgngrp  17850  psgnfix2  17870  relt  17886  ocv0  17943  thlle  17963  thlleval  17964  dsmmval2  18002  frlmip  18044  smadiadetglem1  18318  indistpsx  18455  iuncld  18490  tgrest  18604  resstopn  18631  leordtval2  18657  xkouni  19013  ptclsg  19029  ptuncnv  19221  ptunhmeo  19222  alexsubALTlem4  19463  tsmsf1o  19560  ucnimalem  19696  ressxms  19941  uniretop  20182  cnfldtopn  20202  xrtgioo  20224  zcld  20231  icccmp  20243  xrge0gsumle  20251  xrge0tsms  20252  metnrmlem3  20278  fsum2cn  20288  cnmpt2pc  20341  oprpiece1res1  20364  oprpiece1res2  20365  evth  20372  evth2  20373  om1opn  20449  pi1xfrf  20466  pi1xfrcnv  20470  pi1cof  20472  clsocv  20603  cncmet  20674  cnflduss  20709  rrxprds  20734  ehlbase  20751  ismbl  20850  shftmbl  20861  ioorinv  20897  itg1addlem4  21018  itg2cnlem1  21080  iblitg  21087  itg0  21098  itgss3  21133  ditgneg  21173  limcdif  21192  limciun  21210  dvexp  21268  dvef  21293  dvcnvrelem2  21331  ftc1  21355  mdegfvalOLD  21416  plyremlem  21654  aannenlem2  21679  taylply2  21717  dvradcnv  21770  pserdvlem2  21777  reefgim  21799  cospi  21818  sincos6thpi  21861  tanregt0  21879  dflog2  21896  logfac  21933  dvlog  21980  cxpexp  21997  cxpmul2  22018  cxpsqr  22032  dvsqr  22066  cxpcn2  22068  ang180lem2  22090  isosctrlem2  22101  1cubrlem  22120  1cubr  22121  quart1lem  22134  atancj  22189  atanlogaddlem  22192  atansopn  22211  leibpilem2  22220  log2cnv  22223  log2ublem3  22227  birthdaylem1  22229  birthdaylem2  22230  birthday  22232  dfarea  22238  wilthlem2  22291  ftalem3  22296  ftalem7  22300  basellem2  22303  ppiprm  22373  ppinprm  22374  chtprm  22375  chtnprm  22376  ppi2  22392  ppi3  22393  ppiub  22427  chtub  22435  bclbnd  22503  bposlem8  22514  lgsdilem  22545  lgsdir2lem1  22546  lgsdir2lem2  22547  lgsdir2lem3  22548  lgsquadlem2  22578  lgsquad2lem2  22582  rplogsum  22660  mulog2sumlem2  22668  pnt2  22746  axsegconlem9  22993  ax5seglem7  23003  usgrares1  23145  cusgrares  23202  eupath2lem3  23422  konigsberg  23430  ex-pw  23458  ex-xp  23465  ex-rn  23469  ablosn  23656  efghgrp  23682  nvvop  23809  nvm  23843  cnims  23910  ip0i  24047  ip1ilem  24048  ipdirilem  24051  ipasslem10  24061  h2hva  24198  h2hsm  24199  h2hvs  24201  axhfvadd-zf  24206  axhvcom-zf  24207  axhvass-zf  24208  axhv0cl-zf  24209  axhvaddid-zf  24210  axhfvmul-zf  24211  axhvmulid-zf  24212  axhvmulass-zf  24213  axhvdistr1-zf  24214  axhvdistr2-zf  24215  axhvmul0-zf  24216  axhfi-zf  24217  axhis1-zf  24218  axhis2-zf  24219  axhis3-zf  24220  axhis4-zf  24221  axhcompl-zf  24222  normlem0  24333  normlem1  24334  normlem2  24335  normlem4  24337  normlem9  24342  bcseqi  24344  dfhnorm2  24346  norm3difi  24371  normpari  24378  normpar2i  24380  polid2i  24381  polidi  24382  hhba  24391  hhims  24396  hhims2  24397  hhsssh  24492  hhssims  24498  hhssims2  24499  shsval3i  24613  dfch2  24632  cmcm2i  24818  fh2  24844  qlaxr3i  24861  spansnji  24871  pjcji  24909  ho0val  24976  df0op2  24978  hosd1i  25048  hosd2i  25049  eigorthi  25063  hhlnoi  25126  hhnmoi  25127  hhbloi  25128  bra0  25176  nmop0  25212  nmfn0  25213  lnopeq0lem1  25231  lnopunilem1  25236  lnophmlem2  25243  nmopcoadji  25327  pjhmopidm  25409  cvmdi  25550  cdj3lem3  25664  cdj3lem3b  25666  abrexdomjm  25711  iundifdifd  25735  iundifdif  25736  mpt2mptxf  25818  df1stres  25822  df2ndres  25823  fcobijfs  25849  nn0supp  25851  resf1o  25854  fpwrelmapffslem  25856  xrslt  25959  xrsclat  25963  gsumle  26097  xrge0tsmsd  26105  xrge0slmod  26165  tpr2rico  26195  xrge0mulc1cn  26224  lmxrge0  26235  esumpfinvallem  26376  esumcocn  26382  hasheuni  26387  esumcvg  26388  measinblem  26487  ddemeas  26505  aean  26513  sxbrsigalem3  26540  dya2iocival  26541  dya2iocucvr  26552  sxbrsigalem1  26553  sxbrsigalem2  26554  sxbrsigalem5  26556  sxbrsiga  26558  sitgclbn  26576  eulerpartlem1  26597  eulerpartgbij  26602  fibp1  26631  coinfliplem  26708  coinflipprob  26709  ballotlemfval  26719  ballotth  26767  sgnneg  26770  ofs2  26792  plymulx  26796  lgamgulmlem5  26866  lgambdd  26870  derang0  26904  subfacp1lem1  26914  subfacp1lem6  26920  kur14lem7  26947  cvmsss2  27010  cvmliftlem8  27028  cvmliftlem10  27030  ghomgrpilem2  27151  fprod2d  27338  faclim  27398  dfpred3  27481  predidm  27495  tz6.26  27512  dftrpred2  27529  bdayfo  27662  pprodcnveq  27760  dfon4  27770  fobigcup  27777  dfiota3  27800  dfrdg4  27827  dfint3  27829  bpoly2  28046  bpoly3  28047  bpoly4  28048  rankeq1o  28055  ssoninhaus  28141  onint1  28142  rabiun  28253  ptrest  28266  cnambfre  28281  ftc1anclem8  28315  dvcnsqr  28319  refssfne  28407  fnopabco  28457  abrexdom  28465  cncfres  28505  scottexf  28822  scott0f  28823  mapfzcons  28894  eldioph4b  28992  diophren  28994  pwssplit4  29284  pwfi2f1o  29293  frlmpwfi  29295  mendplusgfval  29384  mendmulrfval  29386  mendvscafval  29389  idomodle  29403  cytpval  29419  arearect  29433  areaquad  29434  lhe4.4ex1a  29445  compne  29538  refsum2cnlem1  29601  stoweidlem13  29651  stoweidlem32  29670  stoweidlem62  29700  wallispi2lem2  29710  stirlinglem14  29725  rnfdmpr  29992  wwlknprop  30163  wwlknfi  30213  wlknwwlknvbij  30215  clwwlkvbij  30306  mpt2mptx2  30566  bnj1400  31528  bnj66  31552  bnj882  31618  bj-rababwv  31980  cdleme3d  33445  cdleme7a  33457  cdleme31sdnN  33601  cdlemk45  34161
  Copyright terms: Public domain W3C validator