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

Theorem 3eqtr4a 2859
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, 2eqtrdi 2849 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2836 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791
This theorem is referenced by:  rabsnif  4619  uniintsn  4875  iinvdif  4965  iununi  4984  dmxpid  5764  rnxpid  5997  csbrn  6027  dmsnsnsn  6044  opswap  6053  xpcoid  6109  unizlim  6275  fvco4i  6739  fndmdifcom  6790  fmptsng  6907  fmptsnd  6908  csbov  7178  ordunisuc  7527  offres  7666  1stval2  7688  2ndval2  7689  cnvf1olem  7788  fparlem3  7792  fparlem4  7793  imacosuppOLD  7858  seqomlem1  8069  ecovcom  8386  ecovass  8387  ecovdi  8388  resixpfo  8483  mapunen  8670  cardidm  9372  cardiun  9395  alephcard  9481  cardalephex  9501  cardcf  9663  cfidm  9686  alephsing  9687  itunisuc  9830  itunitc  9832  ituniiun  9833  alephadd  9988  alephreg  9993  pwcfsdom  9994  addcompq  10361  addcomnq  10362  mulcompq  10363  mulcomnq  10364  addassnq  10369  mulassnq  10370  addid1  10809  zeo  12056  xnegneg  12595  xaddcom  12621  xaddid1  12622  xnegdi  12629  xmulid1  12660  xadddilem  12675  ixxin  12743  fzsuc2  12960  expneg  13433  sq01  13582  facp1  13634  bcpasc  13677  hashfzp1  13788  resunimafz0  13799  hashf1lem1  13809  hashf1  13811  ccat1st1st  13975  swrdccatin1  14078  swrdccat3blem  14092  repswsymballbi  14133  cshwmodn  14148  cshwlen  14152  repswcshw  14165  trclun  14365  relexpcnv  14386  relexpaddd  14405  absexp  14656  sqreulem  14711  fsumf1o  15072  fsumadd  15088  fsumrev2  15129  fsumparts  15153  fsumrelem  15154  pwm1geoserOLD  15217  fprodf1o  15292  fprodmul  15306  fproddiv  15307  fprodfac  15319  fallfacfwd  15382  efexp  15446  tanval2  15478  sadeq  15811  smumullem  15831  smumul  15832  gcdcom  15852  gcd0id  15857  gcdass  15885  lcmcom  15927  lcmneg  15937  lcmass  15948  nn0gcdsq  16082  dfphi2  16101  pcneg  16200  setscom  16519  strfvi  16529  setsnid  16531  ressbas  16546  ressinbas  16552  ressress  16554  firest  16698  topnval  16700  xpsfeq  16828  xpsaddlem  16838  xpsvsca  16842  oppchomfval  16976  oppcbas  16980  rescbas  17091  rescco  17094  cofuass  17151  fucbas  17222  fuchom  17223  setccatid  17336  estrccatid  17374  xpcbas  17420  oduleval  17733  oduglb  17741  odulub  17743  ipotset  17759  efmndbas  18028  efmndbasabf  18029  symggrplem  18041  smndex1mndlem  18066  pwmnd  18094  grpinvfvi  18138  cntrval  18441  cntzval  18443  oppgplusfval  18468  snsymgefmndeq  18515  symgvalstruct  18517  pmtrprfval  18607  m1expaddsub  18618  sylow1lem2  18716  sylow3lem1  18744  oppglsm  18759  gsumzsplit  19040  gsum2dlem2  19084  gsumcom2  19088  dprd2dlem2  19155  dprd2da  19157  dmdprdsplit2lem  19160  mgpplusg  19236  mgpress  19243  ringidval  19246  opprmulfval  19371  abvtrivd  19604  sralem  19942  srasca  19946  sravsca  19947  sraip  19948  rlmval  19956  zlmlem  20210  zlmsca  20214  zlmvsca  20215  psgninv  20271  ocvval  20356  thlbas  20385  thlle  20386  thloc  20388  dsmmval2  20425  psrmulr  20622  mplmonmul  20704  mplcoe3  20706  opsrbaslem  20717  opsrtoslem2  20724  psr1val  20815  ply1basfvi  20870  ply1plusgfvi  20871  psr1sca2  20880  evl1fval1lem  20954  mattpos1  21061  mdettpos  21216  smadiadetglem1  21276  tgdif0  21597  indislem  21605  restco  21769  txtopon  22196  txindislem  22238  qtopres  22303  hmphindis  22402  ptuncnv  22412  snclseqg  22721  tsmssplit  22757  ussval  22865  tuslem  22873  setsmsbas  23082  tnglem  23246  tngds  23254  tngtset  23255  pcoass  23629  cphsqrtcl2  23791  rrxcph  23996  ovolunlem1a  24100  ioorinv  24180  itg11  24295  itg1mulc  24308  itg2cnlem1  24365  iblss2  24409  ibladdlem  24423  itgfsum  24430  iblabslem  24431  iblabs  24432  ditgneg  24460  deg1fvi  24686  dgrco  24872  logfac  25192  cxpexp  25259  cxpmul2  25280  cxpsqrt  25294  cxpsqrtth  25320  dvcxp1  25329  dvcxp2  25330  ang180lem1  25395  mcubic  25433  quart1  25442  reasinsin  25482  atanlogaddlem  25499  atantayl2  25524  log2tlbnd  25531  basellem2  25667  basellem3  25668  basellem5  25670  basellem8  25673  dchrmulid2  25836  bcp1ctr  25863  lgsneg  25905  lgsneg1  25906  lgsdir2  25914  lgsdir  25916  lgsdi  25918  lgsquad2lem2  25969  pntleml  26195  motgrp  26337  lmiisolem  26590  ttglem  26670  egrsubgr  27067  iswwlksnon  27639  iswspthsnon  27642  bafval  28387  ipidsq  28493  ipasslem1  28614  pjclem2  29979  cvmdi  30107  imadifxp  30364  2ndimaxp  30409  iundisjcnt  30547  dpfrac1  30594  gsumpart  30740  cycpmco2rn  30817  cyc3genpmlem  30843  resvsca  30954  rspectset  31219  indval2  31383  bayesth  31807  ofcccat  31923  plymulx  31928  subfacp1lem6  32542  satfdm  32726  mvtval  32857  mexval  32859  mexval2  32860  mdvval  32861  mrsubfval  32865  mrsubvrs  32879  msubfval  32881  elmsubrn  32885  mvhfval  32890  mpstval  32892  msrfval  32894  mstaval  32901  mthmval  32932  bccolsum  33081  dfrdg2  33150  dfrdg3  33151  frrlem12  33244  dfrdg4  33522  ordtoplem  33893  ordcmp  33905  curunc  35036  matunitlindflem2  35051  poimirlem6  35060  poimirlem7  35061  poimirlem11  35065  poimirlem12  35066  poimirlem13  35067  poimirlem14  35068  poimirlem16  35070  poimirlem19  35073  poimirlem21  35075  poimirlem22  35076  poimirlem27  35081  poimirlem31  35085  poimirlem32  35086  itg2addnclem2  35106  ibladdnclem  35110  iblabsnclem  35117  iblabsnc  35118  iblmulc2nc  35119  ftc1anclem8  35134  pmodN  37143  tgrpgrplem  38042  tendoplass  38076  tendoicl  38089  erngdvlem3  38283  dvhvaddass  38390  dib0  38457  dib1dim2  38461  diclspsn  38487  cdlemn8  38497  dihopelvalcpre  38541  djhcom  38698  nn0expgcd  39487  kelac2  40004  mendbas  40123  mendsca  40128  mendring  40131  iscard4  40236  relexp01min  40409  relexpaddss  40414  iotain  41116  addrcom  41174  rnsnf  41805  itgsinexplem1  42591  volioc  42609  dirkertrigeqlem1  42735  fourierdlem104  42847  sqwvfoura  42865  sqwvfourb  42866  fzopredsuc  43875  fppr2odd  44244  rngccatidALTV  44608  ringccatidALTV  44671  0dig2pr01  45019  nn0sumshdiglemB  45029
  Copyright terms: Public domain W3C validator