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

Theorem 3eqtr4a 2681
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 2671 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2658 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-cleq 2614
This theorem is referenced by:  rabsnif  4256  uniintsn  4512  iinvdif  4590  iununi  4608  dmxpid  5343  rnxpid  5565  csbrn  5594  dmsnsnsn  5611  opswap  5620  xpcoid  5674  unizlim  5842  fvco4i  6274  fndmdifcom  6320  fmptsng  6431  fmptsnd  6432  csbov  6685  ordunisuc  7029  offres  7160  1stval2  7182  2ndval2  7183  cnvf1olem  7272  fparlem3  7276  fparlem4  7277  imacosupp  7332  seqomlem1  7542  ecovcom  7851  ecovass  7852  ecovdi  7853  resixpfo  7943  mapunen  8126  cardidm  8782  cardiun  8805  alephcard  8890  cardalephex  8910  cardcf  9071  cfidm  9094  alephsing  9095  itunisuc  9238  itunitc  9240  ituniiun  9241  alephadd  9396  alephreg  9401  pwcfsdom  9402  addcompq  9769  addcomnq  9770  mulcompq  9771  mulcomnq  9772  addassnq  9777  mulassnq  9778  addid1  10213  zeo  11460  xnegneg  12042  xaddcom  12068  xaddid1  12069  xnegdi  12075  xmulid1  12106  xadddilem  12121  ixxin  12189  fzsuc2  12395  expneg  12863  sq01  12981  facp1  13060  bcpasc  13103  hashfzp1  13213  resunimafz0  13224  hashf1lem1  13234  hashf1  13236  swrdccatin1  13477  swrdccat3blem  13489  repswsymballbi  13521  cshwmodn  13535  repswcshw  13552  trclun  13749  relexpcnv  13769  absexp  14038  sqreulem  14093  fsumf1o  14448  fsumadd  14464  fsumrev2  14508  fsumparts  14532  fsumrelem  14533  pwm1geoser  14594  fprodf1o  14670  fprodmul  14684  fproddiv  14685  fprodfac  14697  fallfacfwd  14761  efexp  14825  tanval2  14857  sqrt2irrlemOLD  14972  sadeq  15188  smumullem  15208  smumul  15209  gcdcom  15229  gcd0id  15234  gcdass  15258  lcmcom  15300  lcmneg  15310  lcmass  15321  nn0gcdsq  15454  dfphi2  15473  pcneg  15572  setscom  15897  strfvi  15907  setsnid  15909  ressbas  15924  ressinbas  15930  ressress  15932  firest  16087  topnval  16089  xpsfeq  16218  xpsaddlem  16229  xpsvsca  16233  homffval  16344  oppchomfval  16368  oppcbas  16372  rescbas  16483  rescco  16486  cofuass  16543  fucbas  16614  fuchom  16615  setccatid  16728  estrccatid  16766  xpcbas  16812  xpchomfval  16813  xpccofval  16816  oduleval  17125  oduglb  17133  odulub  17135  ipotset  17151  grpinvfvi  17457  cntrval  17746  cntzval  17748  oppgplusfval  17772  symgbas  17794  symggrp  17814  pmtrprfval  17901  m1expaddsub  17912  sylow1lem2  18008  sylow3lem1  18036  oppglsm  18051  gsumzsplit  18321  gsum2dlem2  18364  gsumcom2  18368  dprd2dlem2  18433  dprd2da  18435  dmdprdsplit2lem  18438  mgpplusg  18487  mgpress  18494  ringidval  18497  opprmulfval  18619  abvtrivd  18834  sralem  19171  srasca  19175  sravsca  19176  sraip  19177  rlmval  19185  psrmulr  19378  mplmonmul  19458  mplcoe3  19460  opsrbaslem  19471  opsrbaslemOLD  19472  opsrtoslem2  19479  psr1val  19550  ply1basfvi  19605  ply1plusgfvi  19606  psr1sca2  19615  evl1fval1lem  19688  zlmlem  19859  zlmsca  19863  zlmvsca  19864  psgninv  19922  ocvval  20005  thlbas  20034  thlle  20035  thloc  20037  dsmmval2  20074  mattpos1  20256  mdettpos  20411  smadiadetglem1  20471  tgdif0  20790  indislem  20798  restco  20962  txtopon  21388  txindislem  21430  qtopres  21495  hmphindis  21594  ptuncnv  21604  snclseqg  21913  tsmssplit  21949  ussval  22057  tuslem  22065  setsmsbas  22274  tnglem  22438  tngds  22446  tngtset  22447  pcoass  22818  cphsqrtcl2  22980  rrxcph  23174  ovolunlem1a  23258  ioorinv  23338  itg11  23452  itg1mulc  23465  itg2cnlem1  23522  iblss2  23566  ibladdlem  23580  itgfsum  23587  iblabslem  23588  iblabs  23589  ditgneg  23615  deg1fvi  23839  dgrco  24025  logfac  24341  cxpexp  24408  cxpmul2  24429  cxpsqrt  24443  dvcxp1  24475  dvcxp2  24476  ang180lem1  24533  mcubic  24568  quart1  24577  reasinsin  24617  atanlogaddlem  24634  atantayl2  24659  log2tlbnd  24666  basellem2  24802  basellem3  24803  basellem5  24805  basellem8  24808  dchrmulid2  24971  bcp1ctr  24998  lgsneg  25040  lgsneg1  25041  lgsdir2  25049  lgsdir  25051  lgsdi  25053  lgsquad2lem2  25104  pntleml  25294  motgrp  25432  lmiisolem  25682  ttglem  25750  egrsubgr  26163  iswwlksnon  26734  iswspthsnon  26735  bafval  27443  ipidsq  27549  ipasslem1  27670  pjclem2  29039  cvmdi  29167  imadifxp  29398  iundisjcnt  29542  dpfrac1  29584  dpfrac1OLD  29585  resvsca  29815  indval2  30061  bayesth  30486  plymulx  30610  subfacp1lem6  31152  mvtval  31382  mexval  31384  mexval2  31385  mdvval  31386  mrsubfval  31390  mrsubvrs  31404  msubfval  31406  elmsubrn  31410  mvhfval  31415  mpstval  31417  msrfval  31419  mstaval  31426  mthmval  31457  bccolsum  31611  dfrdg2  31685  dfrdg3  31686  dfrdg4  32042  ordtoplem  32418  ordcmp  32430  curunc  33371  matunitlindflem2  33386  poimirlem6  33395  poimirlem7  33396  poimirlem11  33400  poimirlem12  33401  poimirlem13  33402  poimirlem14  33403  poimirlem16  33405  poimirlem19  33408  poimirlem21  33410  poimirlem22  33411  poimirlem27  33416  poimirlem31  33420  poimirlem32  33421  itg2addnclem2  33442  ibladdnclem  33446  iblabsnclem  33453  iblabsnc  33454  iblmulc2nc  33455  ftc1anclem8  33472  pmodN  34962  tgrpgrplem  35863  tendoplass  35897  tendoicl  35910  erngdvlem3  36104  dvhvaddass  36212  dib0  36279  dib1dim2  36283  diclspsn  36309  cdlemn8  36319  dihopelvalcpre  36363  djhcom  36520  kelac2  37461  mendbas  37580  mendsca  37585  mendring  37588  relexp01min  37831  relexpaddss  37836  iotain  38444  addrcom  38505  itgsinexplem1  39938  volioc  39957  dirkertrigeqlem1  40084  fourierdlem104  40196  sqwvfoura  40214  sqwvfourb  40215  opidg  41066  fzopredsuc  41102  rngccatidALTV  41760  ringccatidALTV  41823  0dig2pr01  42175  nn0sumshdiglemB  42185
  Copyright terms: Public domain W3C validator