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

Theorem 3eqtr4a 2666
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 2656 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2643 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-cleq 2599
This theorem is referenced by:  rabsnif  4198  uniintsn  4440  iinvdif  4519  iununi  4537  dmxpid  5250  rnxpid  5469  csbrn  5497  dmsnsnsn  5514  opswap  5523  xpcoid  5576  unizlim  5744  fvco4i  6168  fndmdifcom  6212  fmptsng  6314  fmptsnd  6315  csbov  6561  ordunisuc  6898  offres  7028  1stval2  7050  2ndval2  7051  cnvf1olem  7136  fparlem3  7140  fparlem4  7141  imacosupp  7196  seqomlem1  7406  ecovcom  7715  ecovass  7716  ecovdi  7717  resixpfo  7806  mapunen  7988  cardidm  8642  cardiun  8665  alephcard  8750  cardalephex  8770  cardcf  8931  cfidm  8954  alephsing  8955  itunisuc  9098  itunitc  9100  ituniiun  9101  alephadd  9252  alephreg  9257  pwcfsdom  9258  addcompq  9625  addcomnq  9626  mulcompq  9627  mulcomnq  9628  addassnq  9633  mulassnq  9634  addid1  10064  zeo  11292  xnegneg  11875  xaddcom  11900  xaddid1  11901  xnegdi  11904  xmulid1  11935  xadddilem  11950  ixxin  12016  fzsuc2  12220  expneg  12682  sq01  12800  facp1  12879  bcpasc  12922  hashfzp1  13027  hashf1lem1  13045  hashf1  13047  swrdccatin1  13277  swrdccat3blem  13289  repswsymballbi  13321  cshwmodn  13335  repswcshw  13352  trclun  13546  relexpcnv  13566  absexp  13835  sqreulem  13890  fsumf1o  14244  fsumadd  14260  fsumrev2  14299  fsumparts  14322  fsumrelem  14323  pwm1geoser  14382  fprodf1o  14458  fprodmul  14472  fproddiv  14473  fprodfac  14485  fallfacfwd  14549  efexp  14613  tanval2  14645  sqr2irrlem  14759  sadeq  14975  smumullem  14995  smumul  14996  gcdcom  15016  gcd0id  15021  gcdass  15045  lcmcom  15087  lcmneg  15097  lcmass  15108  nn0gcdsq  15241  dfphi2  15260  pcneg  15359  setscom  15674  strfvi  15684  setsnid  15686  ressbas  15700  ressinbas  15706  ressress  15708  firest  15859  topnval  15861  xpsfeq  15990  xpsaddlem  16001  xpsvsca  16005  homffval  16116  oppchomfval  16140  oppcbas  16144  rescbas  16255  rescco  16258  cofuass  16315  fucbas  16386  fuchom  16387  setccatid  16500  estrccatid  16538  xpcbas  16584  xpchomfval  16585  xpccofval  16588  oduleval  16897  oduglb  16905  odulub  16907  ipotset  16923  grpinvfvi  17229  cntrval  17518  cntzval  17520  oppgplusfval  17544  symgbas  17566  symggrp  17586  pmtrprfval  17673  m1expaddsub  17684  sylow1lem2  17780  sylow3lem1  17808  oppglsm  17823  gsumzsplit  18093  gsum2dlem2  18136  gsumcom2  18140  dprd2dlem2  18205  dprd2da  18207  dmdprdsplit2lem  18210  mgpplusg  18259  mgpress  18266  ringidval  18269  opprmulfval  18391  abvtrivd  18606  sralem  18941  srasca  18945  sravsca  18946  sraip  18947  rlmval  18955  psrmulr  19148  mplmonmul  19228  mplcoe3  19230  opsrbaslem  19241  opsrbaslemOLD  19242  opsrtoslem2  19249  psr1val  19320  ply1basfvi  19375  ply1plusgfvi  19376  psr1sca2  19385  evl1fval1lem  19458  zlmlem  19626  zlmsca  19630  zlmvsca  19631  psgninv  19689  ocvval  19769  thlbas  19798  thlle  19799  thloc  19801  dsmmval2  19838  mattpos1  20020  mdettpos  20175  smadiadetglem1  20235  tgdif0  20546  indislem  20553  restco  20717  txtopon  21143  txindislem  21185  qtopres  21250  hmphindis  21349  ptuncnv  21359  snclseqg  21668  tsmssplit  21704  ussval  21812  tuslem  21820  setsmsbas  22028  tnglem  22189  tngds  22197  tngtset  22198  pcoass  22560  cphsqrtcl2  22715  rrxcph  22902  ovolunlem1a  22985  ioorinv  23064  itg11  23178  itg1mulc  23191  itg2cnlem1  23248  iblss2  23292  ibladdlem  23306  itgfsum  23313  iblabslem  23314  iblabs  23315  ditgneg  23341  deg1fvi  23563  dgrco  23749  logfac  24065  cxpexp  24128  cxpmul2  24149  cxpsqrt  24163  dvcxp1  24195  dvcxp2  24196  ang180lem1  24253  mcubic  24288  quart1  24297  reasinsin  24337  atanlogaddlem  24354  atantayl2  24379  log2tlbnd  24386  basellem2  24522  basellem3  24523  basellem5  24525  basellem8  24528  dchrmulid2  24691  bcp1ctr  24718  lgsneg  24760  lgsneg1  24761  lgsdir2  24769  lgsdir  24771  lgsdi  24773  lgsquad2lem2  24824  pntleml  25014  motgrp  25153  lmiisolem  25403  ttglem  25471  eupath2lem3  26269  bafval  26624  ipidsq  26750  ipasslem1  26873  pjclem2  28242  cvmdi  28370  imadifxp  28599  iundisjcnt  28747  resvsca  28964  indval2  29207  bayesth  29631  plymulx  29754  subfacp1lem6  30224  mvtval  30454  mexval  30456  mexval2  30457  mdvval  30458  mrsubfval  30462  mrsubvrs  30476  msubfval  30478  elmsubrn  30482  mvhfval  30487  mpstval  30489  msrfval  30491  mstaval  30498  mthmval  30529  bccolsum  30681  dfrdg2  30748  dfrdg3  30749  dfrdg4  31031  ordtoplem  31407  ordcmp  31419  curunc  32361  matunitlindflem2  32376  poimirlem6  32385  poimirlem7  32386  poimirlem11  32390  poimirlem12  32391  poimirlem13  32392  poimirlem14  32393  poimirlem16  32395  poimirlem19  32398  poimirlem21  32400  poimirlem22  32401  poimirlem27  32406  poimirlem31  32410  poimirlem32  32411  itg2addnclem2  32432  ibladdnclem  32436  iblabsnclem  32443  iblabsnc  32444  iblmulc2nc  32445  ftc1anclem8  32462  pmodN  33954  tgrpgrplem  34855  tendoplass  34889  tendoicl  34902  erngdvlem3  35096  dvhvaddass  35204  dib0  35271  dib1dim2  35275  diclspsn  35301  cdlemn8  35311  dihopelvalcpre  35355  djhcom  35512  kelac2  36453  mendbas  36573  mendsca  36578  mendring  36581  relexp01min  36824  relexpaddss  36829  iotain  37440  addrcom  37500  itgsinexplem1  38646  volioc  38665  dirkertrigeqlem1  38792  fourierdlem104  38904  sqwvfoura  38922  sqwvfourb  38923  fzopredsuc  39748  opidg  40121  resunimafz0  40192  uhgrstrrepe  40303  egrsubgr  40500  iswwlksnon  41050  iswspthsnon  41051  rngccatidALTV  41780  ringccatidALTV  41843  0dig2pr01  42201  nn0sumshdiglemB  42211  dpfrac1  42272  dpfrac1OLD  42273
  Copyright terms: Public domain W3C validator