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

Theorem eqtr4i 2487
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 2471 . 2  |-  B  =  C
41, 3eqtri 2484 1  |-  A  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-cleq 2455
This theorem is referenced by:  3eqtr2i  2490  3eqtr2ri  2491  3eqtr4i  2494  3eqtr4ri  2495  rabab  3077  cbvralcsf  3407  cbvrabcsf  3410  dfin5  3424  dfdif2  3425  uneqin  3706  unrab  3726  inrab  3727  inrab2  3728  difrab  3729  dfrab3ss  3733  rabun2  3734  rabxm  3767  elnelun  3770  difidALT  3848  difdifdir  3867  dfif3  3907  dfif5  3909  rabsnif  4054  tpidm  4089  ssunpr  4147  sstp  4149  dfint2  4250  iunrab  4339  uniiun  4345  intiin  4346  0iin  4350  mptv  4512  dfepfr  4841  epfrc  4842  xpundi  4909  xpundir  4910  csbcnv  5040  resiun2  5146  resopab  5173  opabresid  5180  dffr3  5223  dfse2  5224  cnvun  5263  imaundir  5271  imainrect  5300  cnvcnv2  5312  cnvcnvres  5322  dmtpop  5335  rnsnopg  5338  rnco2  5365  dmco  5366  co01  5373  unidmrn  5389  dfdm2  5391  predidm  5425  tz6.26  5434  dfmpt3  5724  mptun  5735  funcocnv2  5865  dffv2  5966  fnasrn  6099  fpr  6101  fmptap  6116  riotav  6287  dmoprab  6409  rnoprab2  6412  mpt2v  6418  mpt2mptx  6419  abrexex2g  6802  abrexex2  6806  1stval2  6842  2ndval2  6843  fo1st  6845  fo2nd  6846  xp2  6860  dfoprab4f  6883  offval22  6904  fmpt2co  6911  tposmpt2  7041  tposconst  7042  recsfval  7130  rdgsucmpt2  7179  frsucmpt2  7188  df2o3  7226  o1p1e2  7273  oarec  7294  omopthlem2  7388  ecqs  7458  qliftf  7482  erovlem  7490  mapsnf1o3  7551  ixp0x  7581  omf1o  7706  xpf1o  7765  mapunen  7772  enp1ilem  7836  pwfi  7900  marypha1lem  7978  marypha2lem4  7983  dfoi  8057  infeq5i  8172  oemapso  8218  cantnflem1  8225  rankelop  8376  leweon  8473  r0weon  8474  kmlem11  8621  infcda1  8654  ackbij1lem16  8696  cf0  8712  cfsmolem  8731  alephsuc3  9036  fpwwe  9102  canthp1lem1  9108  wuncval2  9203  prlem936  9503  m1p1sr  9547  m1m1sr  9548  dfcnqs  9597  ssxr  9734  mul02lem2  9841  addid1  9844  3m1e2  10759  4m1e3  10760  2p2e4  10761  3p2e5  10776  3p3e6  10777  4p2e6  10778  4p3e7  10779  4p4e8  10780  5p2e7  10781  5p3e8  10782  5p4e9  10783  5p5e10  10784  6p2e8  10785  6p3e9  10786  6p4e10  10787  7p2e9  10788  7p3e10  10789  8p2e10  10790  nnzrab  10999  nn0zrab  11000  dec0u  11100  dec0h  11101  decsuc  11108  decsucc  11112  numma  11116  decma  11123  decmac  11124  decma2c  11125  decadd  11126  decaddc  11127  decmul1c  11132  decmul2c  11133  5t5e25  11161  6t6e36  11166  8t6e48  11177  nn0uz  11227  nnuz  11228  xaddcom  11565  x2times  11619  ioomax  11743  iccmax  11744  ioopos  11745  ioorp  11746  prunioo  11796  fseq1p1m1  11903  fzo13pr  12034  fzo0to2pr  12035  fzo0to3tp  12036  om2uzrdg  12208  fzennn  12219  irec  12412  facnn  12499  fac0  12500  faclbnd2  12514  faclbnd4lem1  12516  hashfun  12648  hashbclem  12654  hashf1lem1  12657  hashf1lem2  12658  fz1isolem  12663  swrdccatin1  12882  swrdccat3blem  12894  s1co  12973  s2eq2s1eq  13070  dfid5  13145  dfid6  13146  fsumrev2  13898  fsumparts  13921  fsumiun  13936  isumnn0nn  13955  harmonic  13972  0.999...  13992  fprod2d  14090  bpoly2  14165  bpoly3  14166  bpoly4  14167  ege2le3  14199  cos1bnd  14296  efieq1re  14308  eirrlem  14311  qnnen  14321  cpnnen  14336  ruclem6  14342  3dvds  14424  m1bits  14469  algrp1  14588  phiprmpw  14779  prmreclem4  14918  4sqlem11  14954  4sqlem19  14968  dec5dvds  15091  decsplit1  15109  5prm  15135  7prm  15137  1259lem2  15158  1259lem3  15159  1259lem4  15160  1259lem5  15161  1259prm  15162  2503lem1  15163  2503lem2  15164  2503lem3  15165  2503prm  15166  4001lem1  15167  4001lem2  15168  4001lem3  15169  4001lem4  15170  4001prm  15171  ndxid  15197  strle1  15276  grpbasex  15295  grpplusgx  15296  quslem  15504  xpslem  15534  acsfn1  15622  acsfn2  15624  comfffval2  15661  xpchomfval  16119  xpccofval  16122  1stfval  16131  2ndfval  16134  oduleg  16433  ismgmid  16562  grpinvfvi  16762  gaorb  17016  cntri  17039  cntrsubgnsg  17049  cntrnsg  17050  oppglem  17056  oppgcntr  17071  gsumwrev  17072  symgbas  17076  symgga  17102  cayleylem1  17108  psgnunilem2  17191  efgval2  17429  efgredlemc  17450  efgcpbllema  17459  frgpnabllem1  17564  gsumzaddlem  17609  mgplem  17783  opprlem  17911  oppr0  17916  opprneg  17918  rlmscaf  18486  mplbas  18708  mpladd  18721  mplmul  18722  mplvsca2  18725  ressmplbas2  18734  ltbwe  18751  evlslem4  18786  psr1bas2  18838  ply1bas  18843  ply1assa  18847  mplplusg  18868  mplmulr  18869  psr1plusg  18870  psr1vsca  18871  psr1mulr  18872  ply1plusg  18873  ply1vsca  18874  ply1mulr  18875  ply1mpl0  18903  ply1mpl1  18905  coe1mul  18918  xrsds  19066  gsumfsum  19089  zringunit  19117  cnmsgngrp  19202  psgnfix2  19222  relt  19238  ocv0  19295  thlle  19315  thlleval  19316  dsmmval2  19354  frlmip  19391  matgsum  19517  smadiadetglem1  19751  indistpsx  20080  iuncld  20115  tgrest  20230  resstopn  20257  leordtval2  20283  xkouni  20669  ptclsg  20685  ptuncnv  20877  ptunhmeo  20878  alexsubALTlem4  21120  tsmsf1o  21214  ucnimalem  21350  ressxms  21595  uniretop  21838  cnfldtopn  21857  xrtgioo  21879  zcld  21886  icccmp  21898  xrge0gsumle  21906  xrge0tsms  21907  metnrmlem3  21933  metnrmlem3OLD  21948  fsum2cn  21958  cnmpt2pc  22011  oprpiece1res1  22034  oprpiece1res2  22035  evth  22042  evth2  22043  om1opn  22122  pi1xfrf  22139  pi1xfrcnv  22143  pi1cof  22145  clsocv  22276  cncmet  22345  cnflduss  22378  rrxprds  22403  ehlbase  22420  ismbl  22535  shftmbl  22547  ioorinv  22584  ioorinvOLD  22589  itg1addlem4  22713  itg2cnlem1  22775  iblitg  22782  itg0  22793  itgss3  22828  ditgneg  22868  limcdif  22887  limciun  22905  dvexp  22963  dvef  22988  dvcnvrelem2  23026  ftc1  23050  plyremlem  23313  aannenlem2  23341  taylply2  23379  dvradcnv  23432  pserdvlem2  23439  reefgim  23461  cospi  23483  sincos6thpi  23526  tanregt0  23544  dflog2  23566  logfac  23606  dvlog  23652  cxpexp  23669  cxpmul2  23690  cxpsqrt  23704  dvsqrt  23738  dvcnsqrt  23740  cxpcn2  23742  ang180lem2  23795  isosctrlem2  23804  1cubrlem  23823  1cubr  23824  quart1lem  23837  atancj  23892  atanlogaddlem  23895  atansopn  23914  leibpilem2  23923  log2cnv  23926  log2ublem3  23930  birthdaylem1  23933  birthdaylem2  23934  birthday  23936  dfarea  23942  lgamgulmlem5  24014  lgambdd  24018  wilthlem2  24050  ftalem3  24055  ftalem7  24061  basellem2  24064  ppiprm  24134  ppinprm  24135  chtprm  24136  chtnprm  24137  ppi2  24153  ppi3  24154  ppiub  24188  chtub  24196  bclbnd  24264  bposlem8  24275  lgsdilem  24306  lgsdir2lem1  24307  lgsdir2lem2  24308  lgsdir2lem3  24309  lgsquadlem2  24339  lgsquad2lem2  24343  rplogsum  24421  mulog2sumlem2  24429  pnt2  24507  istrkg2ld  24564  axsegconlem9  25011  ax5seglem7  25021  usgrares1  25194  cusgrares  25256  wwlknprop  25470  wwlknfi  25522  wlknwwlknvbij  25524  clwwlkvbij  25585  eupath2lem3  25763  konigsberg  25771  ex-pw  25935  ex-xp  25942  ex-rn  25946  ablosn  26131  efghgrpOLD  26157  nvvop  26284  nvm  26318  cnims  26385  ip0i  26522  ip1ilem  26523  ipdirilem  26526  ipasslem10  26536  h2hva  26683  h2hsm  26684  h2hvs  26686  axhfvadd-zf  26691  axhvcom-zf  26692  axhvass-zf  26693  axhv0cl-zf  26694  axhvaddid-zf  26695  axhfvmul-zf  26696  axhvmulid-zf  26697  axhvmulass-zf  26698  axhvdistr1-zf  26699  axhvdistr2-zf  26700  axhvmul0-zf  26701  axhfi-zf  26702  axhis1-zf  26703  axhis2-zf  26704  axhis3-zf  26705  axhis4-zf  26706  axhcompl-zf  26707  normlem0  26818  normlem1  26819  normlem2  26820  normlem4  26822  normlem9  26827  bcseqi  26829  dfhnorm2  26831  norm3difi  26856  normpari  26863  normpar2i  26865  polid2i  26866  polidi  26867  hhba  26876  hhims  26881  hhims2  26882  hhsssh  26976  hhssims  26982  hhssims2  26983  shsval3i  27097  dfch2  27116  cmcm2i  27302  fh2  27328  qlaxr3i  27345  spansnji  27355  pjcji  27393  ho0val  27459  df0op2  27461  hosd1i  27531  hosd2i  27532  eigorthi  27546  hhlnoi  27609  hhnmoi  27610  hhbloi  27611  bra0  27659  nmop0  27695  nmfn0  27696  lnopeq0lem1  27714  lnopunilem1  27719  lnophmlem2  27726  nmopcoadji  27810  pjhmopidm  27892  cvmdi  28033  cdj3lem3  28147  cdj3lem3b  28149  abrexdomjm  28197  uniin1  28219  uniin2  28220  iundifdifd  28231  iundifdif  28232  mpt2mptxf  28332  df1stres  28336  df2ndres  28337  fcobijfs  28363  resf1o  28367  fpwrelmapffslem  28369  xrslt  28490  xrsclat  28494  gsumle  28593  xrge0tsmsd  28599  xrge0slmod  28658  fimaproj  28711  circtopn  28715  tpr2rico  28769  xrge0mulc1cn  28798  lmxrge0  28809  esumpfinvallem  28946  esumcocn  28952  hasheuni  28957  esumcvg  28958  rossros  29053  measinblem  29093  aean  29117  sxbrsigalem3  29144  dya2iocival  29145  dya2iocucvr  29156  sxbrsigalem1  29157  sxbrsigalem2  29158  sxbrsigalem5  29160  sxbrsiga  29162  fiunelcarsg  29198  eulerpartlem1  29250  eulerpartgbij  29255  fibp1  29284  coinfliplem  29361  coinflipprob  29362  ballotlemfval  29372  ballotth  29420  ballotthOLD  29458  sgnneg  29461  ofs2  29483  plymulx  29487  bnj1400  29697  bnj66  29721  bnj882  29787  derang0  29942  subfacp1lem1  29952  subfacp1lem6  29958  kur14lem7  29985  cvmsss2  30047  cvmliftlem8  30065  cvmliftlem10  30067  msubfval  30212  quad3  30352  ghomgrpilem2  30354  bcprod  30424  bccolsum  30425  faclim  30432  dftrpred2  30510  bdayfo  30614  pprodcnveq  30700  dfon4  30710  fobigcup  30717  dfiota3  30740  dfrecs2  30767  dfrdg4  30768  dfint3  30769  rankeq1o  30988  refssfne  31064  ssoninhaus  31158  onint1  31159  bj-rababwv  31522  bj-inrab3  31578  rnmptsn  31783  dissneq  31789  dffinxpf  31823  finxpreclem4  31832  rabiun  31972  ptrest  31985  poimirlem3  31989  poimirlem4  31990  poimirlem13  31999  poimirlem16  32002  poimirlem22  32008  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  poimirlem30  32016  cnambfre  32035  ftc1anclem8  32070  fnopabco  32095  abrexdom  32103  cncfres  32143  scottexf  32457  scott0f  32458  cdleme3d  33843  cdleme7a  33855  cdleme31sdnN  34000  cdlemk45  34560  mapfzcons  35604  eldioph4b  35700  diophren  35702  pwssplit4  35993  pwfi2f1o  36000  frlmpwfi  36002  mendplusgfval  36097  mendmulrfval  36099  mendvscafval  36102  idomodle  36116  cytpval  36132  arearect  36146  relintab  36235  dfid7  36265  cnvrcl0  36278  dfrtrcl5  36282  dfrcl3  36313  dfrcl4  36314  comptiunov2i  36344  corcltrcl  36377  inductionexd  36639  nznngen  36710  hashnzfz2  36715  lhe4.4ex1a  36723  dvradcnv2  36741  binomcxplemrat  36744  binomcxplemnotnn0  36750  compne  36838  refsum2cnlem1  37399  fiiuncl  37445  rnmptc  37491  iccdifprioo  37702  lptre2pt  37806  limclner  37818  stoweidlem13  37974  stoweidlem32  37994  stoweidlem62  38024  stoweidlem62OLD  38025  wallispi2lem2  38035  stirlinglem14  38050  dirkertrigeqlem1  38061  dirkercncflem4  38069  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem73  38144  fourierdlem81  38152  fourierdlem92  38163  fourierdlem103  38174  fourierdlem104  38175  fouriercnp  38191  fouriersw  38196  sge0tsms  38325  sge0iunmptlemfi  38358  ovolval5lem3  38583  opoeALTV  38947  evengpop3  39028  rnfdmpr  39153  nbgrnvtx0  39555  nbgrel  39556  rusgrprc  39751  cznabel  40325  cznrng  40326  mpt2mptx2  40485
  Copyright terms: Public domain W3C validator