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

Theorem 3eqtr4i 2496
Description: An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1
3eqtr4i.2
3eqtr4i.3
Assertion
Ref Expression
3eqtr4i

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2
2 3eqtr4i.3 . . 3
3 3eqtr4i.1 . . 3
42, 3eqtr4i 2489 . 2
51, 4eqtr4i 2489 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395
This theorem is referenced by:  rabswap  3037  rabbiia  3098  cbvrab  3107  cbvcsb  3439  csbco  3444  cbvrabcsf  3469  un4  3663  in13  3710  in31  3711  in4  3713  indifcom  3742  indir  3745  undir  3746  difdif2  3754  notrab  3774  dfnul3  3787  rab0  3806  dfif5  3957  rabsnifsb  4098  prcom  4108  tprot  4125  tpcoma  4126  tpcomb  4127  tpass  4128  qdassr  4130  pw0  4177  pwpw0  4178  opid  4236  pwsn  4243  pwsnALT  4244  int0  4300  rabasiun  4334  cbviun  4367  cbviin  4368  iunrab  4377  iunin1  4395  iinuni  4414  cbvopab  4520  cbvopab1  4522  cbvopab2  4523  cbvopab1s  4524  cbvopab2v  4526  unopab  4527  cbvmpt  4542  iunopab  4788  dfid3  4801  rabxp  5041  fconstmpt  5048  csbxp  5086  inxp  5140  cnvco  5193  csbdm  5202  rnmpt  5253  csbres  5281  resundi  5292  resundir  5293  resindi  5294  resindir  5295  rescom  5303  resima  5311  imadmrn  5352  cnvimarndm  5363  cnvi  5415  cnvin  5418  rnun  5419  imaundi  5423  cnvxp  5429  imainrect  5453  csbrn  5473  imacnvcnv  5477  resdmres  5503  imadmres  5504  mptpreima  5505  cbviota  5561  sb8iota  5563  resdif  5841  opabiotadm  5935  fndmin  5994  fninfp  6098  cbvriota  6267  dfoprab2  6343  cbvoprab1  6369  cbvoprab2  6370  cbvoprab12  6371  cbvoprab3  6373  cbvmpt2x  6375  resoprab  6398  caov32  6502  caov31  6504  caov4  6506  caovlem2  6511  uniuni  6609  zfrep6  6768  ofmres  6796  dfopab2  6854  dfxp3  6860  dmmpt2ssx  6865  fmpt2x  6866  fsplit  6905  ovtpos  6989  tposco  7005  tfrlem10  7075  mapsncnv  7485  cbvixp  7506  xpcomco  7627  sbthlem6  7652  1sdom  7742  dfsup3OLD  7924  cardf2  8345  alephcard  8472  alephfplem1  8506  pwcda1  8595  ackbij1lem14  8634  compsscnv  8772  dffin1-5  8789  ituniiun  8823  axdc2lem  8849  axdc3lem4  8854  axcclem  8858  pwcfsdom  8979  dmaddpi  9289  dmmulpi  9290  adderpqlem  9353  addassnq  9357  mulcanenq  9359  addcmpblnr  9467  mulcmpblnrlem  9468  ltsrpr  9475  mulgt0sr  9503  sqgt0sr  9504  axi2m1  9557  negiso  10544  nummac  11036  fzprval  11769  fztpval  11770  seqval  12118  sqrecii  12250  sqdivi  12252  binom2i  12277  hashgval  12408  revs1  12739  cats1cat  12826  shftdm  12904  shftidt2  12914  cji  12992  cbvsum  13517  sumfc  13531  ackbijnn  13640  cbvprod  13722  prodfc  13752  divalglem2  14053  nn0gcdsq  14285  prmreclem2  14435  prmrec  14440  hashbc0  14523  dec5nprm  14552  dec2nprm  14553  gcdi  14559  decexp2  14561  decsplit  14569  1259lem1  14613  1259lem4  14616  4001lem1  14623  strlemor2  14725  strlemor3  14726  phlstr  14778  lubdm  15609  glbdm  15622  oduval  15760  oduleval  15761  odubas  15763  oppgid  16391  symgbas0  16419  gsumcom2  17003  ringidval  17155  oppr1  17283  dfrhm2  17366  opsrtoslem1  18148  cnfldsub  18446  cnflddiv  18448  dvdsrzring  18507  dvdsrz  18508  pjdm  18738  pjfval2  18740  restco  19665  cnmptid  20162  ufprim  20410  tgioo3  21310  oprpiece1res1  21451  oprpiece1res2  21452  volfiniun  21957  vitalilem4  22020  cbvitg  22182  itgresr  22185  iblcnlem1  22194  cbvditg  22258  sincos3rdpi  22909  ang180lem2  23142  1cubrlem  23172  asin1  23225  log2ublem2  23278  log2ublem3  23279  emcllem5  23329  lgsdir2lem5  23602  lgsquadlem3  23631  cchhllem  24190  ax5seglem7  24238  axlowdimlem4  24248  usgraop  24350  usgrafilem1  24411  cusgrasizeindslem2  24474  vdgrun  24901  vdgrfiun  24902  vdegp1bi  24985  ex-un  25145  ex-pw  25150  ex-cnv  25158  ex-co  25159  bafval  25497  vsfval  25528  cnnvba  25584  cnnvm  25588  ip2dii  25759  siilem1  25766  h2hcau  25896  hvsubsub4i  25976  hvnegdii  25979  normlem3  26029  normlem8  26034  norm-iii-i  26056  normpar2i  26073  polid2i  26074  chjassi  26404  chj4i  26441  h1de2i  26471  spanunsni  26497  fh3i  26541  fh4i  26542  qlax4i  26548  qlaxr3i  26554  3oalem5  26584  pjadjii  26592  pjsubii  26596  hoadd32i  26697  cnvadj  26811  hh0oi  26822  hhcno  26823  hhcnf  26824  nmopnegi  26884  lnophmlem2  26936  branmfn  27024  rabrab  27399  abrexexd  27407  cbvmptf  27494  maprnin  27554  lmlimxrge0  27930  cbvesum  28054  unibrsiga  28157  eulerpartlemt  28310  eulerpartgbij  28311  ballotlem2  28427  ballotlemrinv  28472  subfacp1lem1  28623  kur14lem2  28651  kur14lem5  28654  kur14lem7  28656  cvmscld  28718  mvtval  28860  mthmpps  28942  dfid4  29103  4bc2eq6  29112  dfpred3  29254  predin  29269  predun  29270  preddif  29271  wfi  29287  frind  29323  symdifcom  29469  fixun  29559  fsumcube  29822  rabiun  30036  ovoliunnfl  30056  voliunnfl  30058  mbfposadd  30062  asindmre  30102  mendsca  31138  areaquad  31184  fprodabs2  31602  stoweidlem13  31795  wallispilem4  31850  fourierdlem94  31983  fourierdlem102  31991  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fourierdlem114  32003  usgfislem1  32444  usgfisALTlem1  32448  cbvmpt2x2  32925  dmmpt2ssx2  32926  zlmodzxzequa  33097  zlmodzxzequap  33100  bnj1146  33850  bnj893  33986  bnj1234  34069  bj-inrab  34495  bj-pr1un  34561  bj-pr2un  34575  cdleme25cv  36084  trclubg  37785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator