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

Theorem 3eqtr4a 2711
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1 𝐴 = 𝐵
3eqtr4a.2 (𝜑𝐶 = 𝐴)
3eqtr4a.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3eqtr4a (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3 (𝜑𝐶 = 𝐴)
2 3eqtr4a.1 . . 3 𝐴 = 𝐵
31, 2syl6eq 2701 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2688 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  rabsnif  4290  uniintsn  4546  iinvdif  4624  iununi  4642  dmxpid  5377  rnxpid  5602  csbrn  5631  dmsnsnsn  5649  opswap  5660  xpcoid  5714  unizlim  5882  fvco4i  6315  fndmdifcom  6362  fmptsng  6475  fmptsnd  6476  csbov  6728  ordunisuc  7074  offres  7205  1stval2  7227  2ndval2  7228  cnvf1olem  7320  fparlem3  7324  fparlem4  7325  imacosupp  7380  seqomlem1  7590  ecovcom  7896  ecovass  7897  ecovdi  7898  resixpfo  7988  mapunen  8170  cardidm  8823  cardiun  8846  alephcard  8931  cardalephex  8951  cardcf  9112  cfidm  9135  alephsing  9136  itunisuc  9279  itunitc  9281  ituniiun  9282  alephadd  9437  alephreg  9442  pwcfsdom  9443  addcompq  9810  addcomnq  9811  mulcompq  9812  mulcomnq  9813  addassnq  9818  mulassnq  9819  addid1  10254  zeo  11501  xnegneg  12083  xaddcom  12109  xaddid1  12110  xnegdi  12116  xmulid1  12147  xadddilem  12162  ixxin  12230  fzsuc2  12436  expneg  12908  sq01  13026  facp1  13105  bcpasc  13148  hashfzp1  13256  resunimafz0  13267  hashf1lem1  13277  hashf1  13279  ccat1st1st  13448  swrdccatin1  13529  swrdccat3blem  13541  repswsymballbi  13573  cshwmodn  13587  repswcshw  13604  trclun  13799  relexpcnv  13819  absexp  14088  sqreulem  14143  fsumf1o  14498  fsumadd  14514  fsumrev2  14558  fsumparts  14582  fsumrelem  14583  pwm1geoser  14644  fprodf1o  14720  fprodmul  14734  fproddiv  14735  fprodfac  14747  fallfacfwd  14811  efexp  14875  tanval2  14907  sqrt2irrlemOLD  15022  sadeq  15241  smumullem  15261  smumul  15262  gcdcom  15282  gcd0id  15287  gcdass  15311  lcmcom  15353  lcmneg  15363  lcmass  15374  nn0gcdsq  15507  dfphi2  15526  pcneg  15625  setscom  15950  strfvi  15960  setsnid  15962  ressbas  15977  ressinbas  15983  ressress  15985  firest  16140  topnval  16142  xpsfeq  16271  xpsaddlem  16282  xpsvsca  16286  homffval  16397  oppchomfval  16421  oppcbas  16425  rescbas  16536  rescco  16539  cofuass  16596  fucbas  16667  fuchom  16668  setccatid  16781  estrccatid  16819  xpcbas  16865  xpchomfval  16866  xpccofval  16869  oduleval  17178  oduglb  17186  odulub  17188  ipotset  17204  grpinvfvi  17510  cntrval  17798  cntzval  17800  oppgplusfval  17824  symgbas  17846  symggrp  17866  pmtrprfval  17953  m1expaddsub  17964  sylow1lem2  18060  sylow3lem1  18088  oppglsm  18103  gsumzsplit  18373  gsum2dlem2  18416  gsumcom2  18420  dprd2dlem2  18485  dprd2da  18487  dmdprdsplit2lem  18490  mgpplusg  18539  mgpress  18546  ringidval  18549  opprmulfval  18671  abvtrivd  18888  sralem  19225  srasca  19229  sravsca  19230  sraip  19231  rlmval  19239  psrmulr  19432  mplmonmul  19512  mplcoe3  19514  opsrbaslem  19525  opsrbaslemOLD  19526  opsrtoslem2  19533  psr1val  19604  ply1basfvi  19659  ply1plusgfvi  19660  psr1sca2  19669  evl1fval1lem  19742  zlmlem  19913  zlmsca  19917  zlmvsca  19918  psgninv  19976  ocvval  20059  thlbas  20088  thlle  20089  thloc  20091  dsmmval2  20128  mattpos1  20310  mdettpos  20465  smadiadetglem1  20525  tgdif0  20844  indislem  20852  restco  21016  txtopon  21442  txindislem  21484  qtopres  21549  hmphindis  21648  ptuncnv  21658  snclseqg  21966  tsmssplit  22002  ussval  22110  tuslem  22118  setsmsbas  22327  tnglem  22491  tngds  22499  tngtset  22500  pcoass  22870  cphsqrtcl2  23032  rrxcph  23226  ovolunlem1a  23310  ioorinv  23390  itg11  23503  itg1mulc  23516  itg2cnlem1  23573  iblss2  23617  ibladdlem  23631  itgfsum  23638  iblabslem  23639  iblabs  23640  ditgneg  23666  deg1fvi  23890  dgrco  24076  logfac  24392  cxpexp  24459  cxpmul2  24480  cxpsqrt  24494  dvcxp1  24526  dvcxp2  24527  ang180lem1  24584  mcubic  24619  quart1  24628  reasinsin  24668  atanlogaddlem  24685  atantayl2  24710  log2tlbnd  24717  basellem2  24853  basellem3  24854  basellem5  24856  basellem8  24859  dchrmulid2  25022  bcp1ctr  25049  lgsneg  25091  lgsneg1  25092  lgsdir2  25100  lgsdir  25102  lgsdi  25104  lgsquad2lem2  25155  pntleml  25345  motgrp  25483  lmiisolem  25733  ttglem  25801  egrsubgr  26214  iswwlksnon  26802  iswwlksnonOLD  26803  iswspthsnon  26806  iswspthsnonOLD  26807  bafval  27587  ipidsq  27693  ipasslem1  27814  pjclem2  29183  cvmdi  29311  imadifxp  29540  iundisjcnt  29685  dpfrac1  29727  dpfrac1OLD  29728  resvsca  29958  indval2  30204  bayesth  30629  plymulx  30753  subfacp1lem6  31293  mvtval  31523  mexval  31525  mexval2  31526  mdvval  31527  mrsubfval  31531  mrsubvrs  31545  msubfval  31547  elmsubrn  31551  mvhfval  31556  mpstval  31558  msrfval  31560  mstaval  31567  mthmval  31598  bccolsum  31751  dfrdg2  31825  dfrdg3  31826  dfrdg4  32183  ordtoplem  32559  ordcmp  32571  curunc  33521  matunitlindflem2  33536  poimirlem6  33545  poimirlem7  33546  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem16  33555  poimirlem19  33558  poimirlem21  33560  poimirlem22  33561  poimirlem27  33566  poimirlem31  33570  poimirlem32  33571  itg2addnclem2  33592  ibladdnclem  33596  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  ftc1anclem8  33622  pmodN  35454  tgrpgrplem  36354  tendoplass  36388  tendoicl  36401  erngdvlem3  36595  dvhvaddass  36703  dib0  36770  dib1dim2  36774  diclspsn  36800  cdlemn8  36810  dihopelvalcpre  36854  djhcom  37011  kelac2  37952  mendbas  38071  mendsca  38076  mendring  38079  relexp01min  38322  relexpaddss  38327  iotain  38935  addrcom  38996  itgsinexplem1  40487  volioc  40506  dirkertrigeqlem1  40633  fourierdlem104  40745  sqwvfoura  40763  sqwvfourb  40764  fzopredsuc  41658  rngccatidALTV  42314  ringccatidALTV  42377  0dig2pr01  42729  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator