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

Theorem eqtr4i 2831
Description: An equality transitivity inference. (Contributed by NM, 26-May-1993.)
Hypotheses
Ref Expression
eqtr4i.1 𝐴 = 𝐵
eqtr4i.2 𝐶 = 𝐵
Assertion
Ref Expression
eqtr4i 𝐴 = 𝐶

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2 𝐴 = 𝐵
2 eqtr4i.2 . . 3 𝐶 = 𝐵
32eqcomi 2815 . 2 𝐵 = 𝐶
41, 3eqtri 2828 1 𝐴 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799
This theorem is referenced by:  3eqtr2i  2834  3eqtr2ri  2835  3eqtr4i  2838  3eqtr4ri  2839  rabab  3417  cbvralcsf  3760  cbvrabcsf  3763  dfin5  3777  dfdif2  3778  uneqin  4080  unrab  4099  inrab  4100  inrab2  4101  difrab  4102  dfrab3ss  4106  rabun2  4107  difidALT  4150  rabxm  4159  elnelun  4162  elnelunOLD  4164  difdifdir  4252  dfif3  4293  dfif5  4295  rabsnif  4449  tpidm  4484  ssunpr  4553  sstp  4555  opidg  4614  dfint2  4671  iunrab  4759  uniiun  4765  intiin  4766  0iin  4770  mptv  4945  dfepfr  5296  epfrc  5297  xpundi  5371  xpundir  5372  csbcnv  5507  resiun2  5621  resopab  5651  opabresid  5667  dffr3  5708  dfse2  5709  cnvun  5749  imaundir  5757  imainrect  5786  cnvcnv2  5799  cnvcnvres  5809  dmtpop  5823  rnsnopg  5826  rnco2  5856  dmco  5857  co01  5864  unidmrn  5879  dfdm2  5881  predidm  5915  tz6.26  5924  dfmpt3  6221  mptun  6232  funcocnv2  6373  dffv2  6488  fnasrn  6630  fpr  6641  fmptap  6657  riotav  6836  dmoprab  6967  rnoprab2  6970  mpt2v  6976  mpt2mptx  6977  abrexex2g  7370  abrexex2OLD  7376  1stval2  7411  2ndval2  7412  fo1st  7414  fo2nd  7415  xp2  7431  dfoprab4f  7454  offval22  7483  fmpt2co  7490  tposmpt2  7620  tposconst  7621  recsfval  7709  rdgsucmpt2  7758  frsucmpt2  7767  df2o3  7806  o1p1e2  7853  o2p2e4  7854  oarec  7875  omopthlem2  7969  ecqs  8042  qliftf  8066  erovlem  8075  mapsnf1o3  8139  ixp0x  8169  omf1o  8298  xpf1o  8357  mapunen  8364  enp1ilem  8429  pwfi  8496  marypha1lem  8574  marypha2lem4  8579  dfoi  8651  infeq5i  8776  oemapso  8822  cantnflem1  8829  rankelop  8980  leweon  9113  r0weon  9114  kmlem11  9263  infcda1  9296  ackbij1lem16  9338  cf0  9354  cfsmolem  9373  alephsuc3  9683  fpwwe  9749  canthp1lem1  9755  wuncval2  9850  prlem936  10150  m1p1sr  10194  m1m1sr  10195  dfcnqs  10244  ssxr  10388  mul02lem2  10494  addid1  10497  2p2e4  11423  3p2e5  11438  3p3e6  11439  4p2e6  11440  4p3e7  11441  4p4e8  11442  5p2e7  11443  5p3e8  11444  5p4e9  11445  6p2e8  11446  6p3e9  11447  7p2e9  11448  nnzrab  11667  nn0zrab  11668  dec0u  11776  dec0h  11777  decsuc  11786  decsucc  11796  numma  11799  decma  11806  decmac  11807  decma2c  11808  decadd  11809  decaddc  11810  decmul1  11819  decmul1c  11820  decmul2c  11821  5p5e10  11826  6p4e10  11827  7p3e10  11830  8p2e10  11835  5t5e25  11858  6t6e36  11863  8t6e48  11874  nn0uz  11936  nnuz  11937  xaddcom  12285  x2times  12343  ioomax  12462  iccmax  12463  ioopos  12464  ioorp  12465  prunioo  12520  fseq1p1m1  12633  fzo13pr  12772  fzo0to2pr  12773  fzo0to3tp  12774  om2uzrdg  12975  fzennn  12987  irec  13183  sq10e99m1  13268  facnn  13278  fac0  13279  faclbnd2  13294  faclbnd4lem1  13296  hashfun  13437  hashbclem  13449  hashf1lem1  13452  hashf1lem2  13453  fz1isolem  13458  swrdccatin1  13703  swrdccat3blem  13715  s1co  13799  s2eq2s1eq  13901  s3eqs2s1eq  13903  ofs2  13931  dfid5  13986  dfid6  13987  fsumrev2  14732  fsumparts  14756  fsumiun  14771  isumnn0nn  14792  harmonic  14809  fprod2d  14928  bpoly2  15004  bpoly3  15005  bpoly4  15006  ege2le3  15036  cos1bnd  15133  efieq1re  15145  eirrlem  15148  qnnen  15158  cpnnen  15174  ruclem6  15180  3dvds  15271  pwp1fsum  15330  m1bits  15377  algrp1  15502  phiprmpw  15694  prmreclem4  15836  4sqlem11  15872  4sqlem19  15880  dec5dvds  15981  decsplit1  15999  5prm  16023  7prm  16025  1259lem2  16046  1259lem3  16047  1259lem4  16048  1259lem5  16049  1259prm  16050  2503lem1  16051  2503lem2  16052  2503lem3  16053  2503prm  16054  4001lem1  16055  4001lem2  16056  4001lem3  16057  4001lem4  16058  4001prm  16059  ndxidOLD  16091  strle1  16180  grpbasex  16201  grpplusgx  16202  quslem  16404  xpslem  16434  acsfn1  16522  acsfn2  16524  comfffval2  16561  xpchomfval  17020  xpccofval  17023  1stfval  17032  2ndfval  17035  oduleg  17333  ismgmid  17465  grpinvfvi  17664  gaorb  17937  cntri  17960  cntrsubgnsg  17970  cntrnsg  17971  oppglem  17977  oppgcntr  17992  gsumwrev  17993  symgbas  17997  symgga  18023  cayleylem1  18029  psgnunilem2  18112  efgval2  18334  efgredlemc  18355  efgcpbllema  18364  frgpnabllem1  18473  gsumzaddlem  18518  mgplem  18692  opprlem  18826  oppr0  18831  opprneg  18833  rmodislmod  19131  rlmscaf  19413  mplbas  19634  mpladd  19647  mplmul  19648  mplvsca2  19651  ressmplbas2  19660  ltbwe  19677  evlslem4  19712  psr1bas2  19764  ply1bas  19769  ply1assa  19773  mplplusg  19794  mplmulr  19795  psr1plusg  19796  psr1vsca  19797  psr1mulr  19798  ply1plusg  19799  ply1vsca  19800  ply1mulr  19801  ply1mpl0  19829  ply1mpl1  19831  coe1mul  19844  xrsds  19993  gsumfsum  20017  zringunit  20040  cnmsgngrp  20128  psgnfix2  20149  relt  20166  ocv0  20227  thlle  20247  thlleval  20248  dsmmval2  20286  frlmip  20323  matgsum  20449  smadiadetglem1  20685  indistpsx  21024  iuncld  21059  tgrest  21173  resstopn  21200  leordtval2  21226  xkouni  21612  ptclsg  21628  ptuncnv  21820  ptunhmeo  21821  alexsubALTlem4  22063  tsmsf1o  22157  ucnimalem  22293  ressxms  22539  uniretop  22775  cnfldtopn  22794  xrtgioo  22818  zcld  22825  icccmp  22837  xrge0gsumle  22845  xrge0tsms  22846  metnrmlem3  22873  fsum2cn  22883  cnmpt2pc  22936  oprpiece1res1  22959  oprpiece1res2  22960  evth  22967  evth2  22968  om1opn  23044  pi1xfrf  23061  pi1xfrcnv  23065  pi1cof  23067  clsocv  23257  cncmet  23327  cnflduss  23360  rrxprds  23385  ehlbase  23402  ismbl  23503  shftmbl  23515  ioorinv  23553  itg1addlem4  23676  itg2cnlem1  23738  iblitg  23745  itg0  23756  itgss3  23791  ditgneg  23831  limcdif  23850  limciun  23868  dvexp  23926  dvef  23953  dvcnvrelem2  23991  ftc1  24015  plyremlem  24269  aannenlem2  24294  taylply2  24332  dvradcnv  24385  pserdvlem2  24392  reefgim  24414  cospi  24435  sincos6thpi  24478  tanregt0  24496  dflog2  24517  logfac  24557  dvlog  24607  cxpexp  24624  cxpmul2  24645  cxpsqrt  24659  dvsqrt  24693  dvcnsqrt  24695  cxpcn2  24697  ang180lem2  24750  isosctrlem2  24759  1cubrlem  24778  1cubr  24779  quart1lem  24792  atancj  24847  atanlogaddlem  24850  atansopn  24869  leibpilem2  24878  log2cnv  24881  log2ublem3  24885  birthdaylem1  24888  birthdaylem2  24889  birthday  24891  dfarea  24897  lgamgulmlem5  24969  lgambdd  24973  wilthlem2  25005  ftalem3  25011  ftalem7  25015  basellem2  25018  ppiprm  25087  ppinprm  25088  chtprm  25089  chtnprm  25090  ppi2  25106  ppi3  25107  ppiub  25139  chtub  25147  bclbnd  25215  bposlem8  25226  lgsdilem  25259  lgsdir2lem1  25260  lgsdir2lem2  25261  lgsdir2lem3  25262  lgsquadlem2  25316  lgsquad2lem2  25320  2lgsoddprmlem3c  25347  rplogsum  25426  mulog2sumlem2  25434  pnt2  25512  istrkg2ld  25569  axsegconlem9  26015  ax5seglem7  26025  iedgedg  26153  uspgrf1oedg  26279  nbgrcl  26439  nbgrnvtx0  26444  rusgrprc  26710  wlkiswwlks2lem4  26995  wlkiswwlks2lem5  26996  wwlksnfi  27039  wlksnwwlknvbijOLD  27042  clwwlkvbij  27278  clwwlkvbijOLDOLD  27279  clwwlkvbijOLD  27280  konigsbergumgr  27420  ex-pw  27613  ex-xp  27620  ex-rn  27624  nvvop  27788  nvm  27820  cnims  27872  ip0i  28004  ip1ilem  28005  ipdirilem  28008  ipasslem10  28018  h2hva  28155  h2hsm  28156  h2hvs  28158  axhfvadd-zf  28163  axhvcom-zf  28164  axhvass-zf  28165  axhv0cl-zf  28166  axhvaddid-zf  28167  axhfvmul-zf  28168  axhvmulid-zf  28169  axhvmulass-zf  28170  axhvdistr1-zf  28171  axhvdistr2-zf  28172  axhvmul0-zf  28173  axhfi-zf  28174  axhis1-zf  28175  axhis2-zf  28176  axhis3-zf  28177  axhis4-zf  28178  axhcompl-zf  28179  normlem0  28290  normlem1  28291  normlem2  28292  normlem4  28294  normlem9  28299  bcseqi  28301  dfhnorm2  28303  norm3difi  28328  normpari  28335  normpar2i  28337  polid2i  28338  polidi  28339  hhba  28348  hhims  28353  hhims2  28354  hhsssh  28450  hhssims  28456  hhssims2  28457  shsval3i  28571  dfch2  28590  cmcm2i  28776  fh2  28802  qlaxr3i  28819  spansnji  28829  pjcji  28867  ho0val  28933  df0op2  28935  hosd1i  29005  hosd2i  29006  eigorthi  29020  hhlnoi  29083  hhnmoi  29084  hhbloi  29085  bra0  29133  nmop0  29169  nmfn0  29170  lnopeq0lem1  29188  lnopunilem1  29193  lnophmlem2  29200  nmopcoadji  29284  pjhmopidm  29366  cvmdi  29507  cdj3lem3  29621  cdj3lem3b  29623  abrexdomjm  29666  uniin1  29688  uniin2  29689  iundifdifd  29701  iundifdif  29702  mpt2mptxf  29800  df1stres  29804  df2ndres  29805  fcobijfs  29824  resf1o  29828  fpwrelmapffslem  29830  dpval3  29923  dp3mul10  29927  dpadd2  29939  dpmul4  29943  xrslt  29997  xrsclat  30001  gsumle  30100  xrge0tsmsd  30106  xrge0slmod  30165  fimaproj  30221  circtopn  30225  tpr2rico  30279  xrge0mulc1cn  30308  lmxrge0  30319  esumpfinvallem  30457  esumcocn  30463  hasheuni  30468  esumcvg  30469  rossros  30564  measinblem  30604  aean  30628  sxbrsigalem3  30655  dya2iocival  30656  dya2iocucvr  30667  sxbrsigalem1  30668  sxbrsigalem2  30669  sxbrsigalem5  30671  sxbrsiga  30673  fiunelcarsg  30699  eulerpartlem1  30750  eulerpartgbij  30755  fibp1  30784  coinfliplem  30861  coinflipprob  30862  ballotlemfval  30872  ballotth  30920  sgnneg  30923  plymulx  30946  circlemethhgt  31042  hgt750lem2  31051  bnj1400  31224  bnj66  31248  bnj882  31314  derang0  31469  subfacp1lem1  31479  subfacp1lem6  31485  kur14lem7  31512  cvmsss2  31574  cvmliftlem8  31592  cvmliftlem10  31594  msubfval  31739  quad3  31881  bcprod  31941  bccolsum  31942  faclim  31949  dftrpred2  32034  frrlem6  32105  frrlem11  32108  bdayfo  32144  pprodcnveq  32306  dfon4  32316  fobigcup  32323  dfiota3  32346  dfrecs2  32373  dfrdg4  32374  dfint3  32375  rankeq1o  32594  refssfne  32669  ssoninhaus  32759  onint1  32760  bj-rababwv  33170  bj-inrab3  33231  rnmptsn  33494  dissneq  33500  dffinxpf  33533  finxpreclem4  33542  cnfinltrel  33552  rabiun  33690  ptrest  33716  poimirlem3  33720  poimirlem4  33721  poimirlem13  33730  poimirlem16  33733  poimirlem22  33739  poimirlem26  33743  poimirlem27  33744  poimirlem30  33747  cnambfre  33765  ftc1anclem8  33799  fnopabco  33824  abrexdom  33832  cncfres  33870  scottexf  34281  scott0f  34282  inres2  34323  dfres4  34373  xrnres  34468  xrnres2  34469  dfcoss2  34479  dfcoss4  34481  1cossres  34492  dmcoss2  34512  1cosscnvxrn  34533  cdleme3d  36006  cdleme7a  36018  cdleme31sdnN  36162  cdlemk45  36722  mapfzcons  37775  eldioph4b  37871  diophren  37873  pwssplit4  38154  pwfi2f1o  38161  frlmpwfi  38163  mendplusgfval  38250  mendmulrfval  38252  mendvscafval  38255  idomodle  38269  cytpval  38282  arearect  38295  relintab  38383  dfid7  38413  cnvrcl0  38426  dfrtrcl5  38430  dfrcl3  38461  dfrcl4  38462  comptiunov2i  38492  corcltrcl  38525  neicvgnvo  38907  inductionexd  38947  nznngen  39009  hashnzfz2  39014  lhe4.4ex1a  39022  dvradcnv2  39040  binomcxplemrat  39043  binomcxplemnotnn0  39049  compneOLD  39137  refsum2cnlem1  39684  fiiuncl  39721  rnmptc  39836  iccdifprioo  40217  lptre2pt  40346  limclner  40357  stoweidlem13  40703  stoweidlem32  40722  stoweidlem62  40752  wallispi2lem2  40762  stirlinglem14  40777  dirkertrigeqlem1  40788  dirkercncflem4  40796  fourierdlem42  40839  fourierdlem73  40869  fourierdlem81  40877  fourierdlem92  40888  fourierdlem103  40899  fourierdlem104  40900  fouriercnp  40916  fouriersw  40921  sge0tsms  41070  sge0iunmptlemfi  41103  ovolval5lem3  41344  cnfsmf  41425  rnfdmpr  41865  fvmptrabdm  41877  m11nprm  42087  opoeALTV  42163  sbgoldbo  42244  evengpop3  42255  cznabel  42516  cznrng  42517  mpt2mptx2  42675  amgmlemALT  43114
  Copyright terms: Public domain W3C validator