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

Theorem 3eqtr4a 2882
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 2872 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2859 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  rabsnif  4653  uniintsn  4906  iinvdif  4994  iununi  5013  dmxpid  5794  rnxpid  6024  csbrn  6054  dmsnsnsn  6071  opswap  6080  xpcoid  6135  unizlim  6301  fvco4i  6756  fndmdifcom  6806  fmptsng  6923  fmptsnd  6924  csbov  7188  ordunisuc  7535  offres  7675  1stval2  7697  2ndval2  7698  cnvf1olem  7796  fparlem3  7800  fparlem4  7801  imacosuppOLD  7866  seqomlem1  8077  ecovcom  8393  ecovass  8394  ecovdi  8395  resixpfo  8489  mapunen  8675  cardidm  9377  cardiun  9400  alephcard  9485  cardalephex  9505  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  12057  xnegneg  12597  xaddcom  12623  xaddid1  12624  xnegdi  12631  xmulid1  12662  xadddilem  12677  ixxin  12745  fzsuc2  12955  expneg  13427  sq01  13576  facp1  13628  bcpasc  13671  hashfzp1  13782  resunimafz0  13793  hashf1lem1  13803  hashf1  13805  ccat1st1st  13974  swrdccatin1  14077  swrdccat3blem  14091  repswsymballbi  14132  cshwmodn  14147  cshwlen  14151  repswcshw  14164  trclun  14364  relexpcnv  14384  absexp  14654  sqreulem  14709  fsumf1o  15070  fsumadd  15086  fsumrev2  15127  fsumparts  15151  fsumrelem  15152  pwm1geoserOLD  15215  fprodf1o  15290  fprodmul  15304  fproddiv  15305  fprodfac  15317  fallfacfwd  15380  efexp  15444  tanval2  15476  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  16517  strfvi  16527  setsnid  16529  ressbas  16544  ressinbas  16550  ressress  16552  firest  16696  topnval  16698  xpsfeq  16826  xpsaddlem  16836  xpsvsca  16840  oppchomfval  16974  oppcbas  16978  rescbas  17089  rescco  17092  cofuass  17149  fucbas  17220  fuchom  17221  setccatid  17334  estrccatid  17372  xpcbas  17418  oduleval  17731  oduglb  17739  odulub  17741  ipotset  17757  pwmnd  18042  grpinvfvi  18086  cntrval  18389  cntzval  18391  oppgplusfval  18416  symgbas  18438  symggrplem  18458  pmtrprfval  18546  m1expaddsub  18557  sylow1lem2  18655  sylow3lem1  18683  oppglsm  18698  gsumzsplit  18978  gsum2dlem2  19022  gsumcom2  19026  dprd2dlem2  19093  dprd2da  19095  dmdprdsplit2lem  19098  mgpplusg  19174  mgpress  19181  ringidval  19184  opprmulfval  19306  abvtrivd  19542  sralem  19880  srasca  19884  sravsca  19885  sraip  19886  rlmval  19894  psrmulr  20094  mplmonmul  20175  mplcoe3  20177  opsrbaslem  20188  opsrtoslem2  20195  psr1val  20284  ply1basfvi  20339  ply1plusgfvi  20340  psr1sca2  20349  evl1fval1lem  20423  zlmlem  20594  zlmsca  20598  zlmvsca  20599  psgninv  20656  ocvval  20741  thlbas  20770  thlle  20771  thloc  20773  dsmmval2  20810  mattpos1  20995  mdettpos  21150  smadiadetglem1  21210  tgdif0  21530  indislem  21538  restco  21702  txtopon  22129  txindislem  22171  qtopres  22236  hmphindis  22335  ptuncnv  22345  snclseqg  22653  tsmssplit  22689  ussval  22797  tuslem  22805  setsmsbas  23014  tnglem  23178  tngds  23186  tngtset  23187  pcoass  23557  cphsqrtcl2  23719  rrxcph  23924  ovolunlem1a  24026  ioorinv  24106  itg11  24221  itg1mulc  24234  itg2cnlem1  24291  iblss2  24335  ibladdlem  24349  itgfsum  24356  iblabslem  24357  iblabs  24358  ditgneg  24384  deg1fvi  24608  dgrco  24794  logfac  25111  cxpexp  25178  cxpmul2  25199  cxpsqrt  25213  cxpsqrtth  25239  dvcxp1  25248  dvcxp2  25249  ang180lem1  25314  mcubic  25352  quart1  25361  reasinsin  25401  atanlogaddlem  25418  atantayl2  25443  log2tlbnd  25451  basellem2  25587  basellem3  25588  basellem5  25590  basellem8  25593  dchrmulid2  25756  bcp1ctr  25783  lgsneg  25825  lgsneg1  25826  lgsdir2  25834  lgsdir  25836  lgsdi  25838  lgsquad2lem2  25889  pntleml  26115  motgrp  26257  lmiisolem  26510  ttglem  26590  egrsubgr  26987  iswwlksnon  27559  iswspthsnon  27562  bafval  28309  ipidsq  28415  ipasslem1  28536  pjclem2  29901  cvmdi  30029  imadifxp  30280  iundisjcnt  30448  dpfrac1  30496  cycpmco2rn  30695  cyc3genpmlem  30721  resvsca  30831  indval2  31173  bayesth  31597  ofcccat  31713  plymulx  31718  subfacp1lem6  32330  satfdm  32514  mvtval  32645  mexval  32647  mexval2  32648  mdvval  32649  mrsubfval  32653  mrsubvrs  32667  msubfval  32669  elmsubrn  32673  mvhfval  32678  mpstval  32680  msrfval  32682  mstaval  32689  mthmval  32720  bccolsum  32869  dfrdg2  32938  dfrdg3  32939  frrlem12  33032  dfrdg4  33310  ordtoplem  33681  ordcmp  33693  curunc  34756  matunitlindflem2  34771  poimirlem6  34780  poimirlem7  34781  poimirlem11  34785  poimirlem12  34786  poimirlem13  34787  poimirlem14  34788  poimirlem16  34790  poimirlem19  34793  poimirlem21  34795  poimirlem22  34796  poimirlem27  34801  poimirlem31  34805  poimirlem32  34806  itg2addnclem2  34826  ibladdnclem  34830  iblabsnclem  34837  iblabsnc  34838  iblmulc2nc  34839  ftc1anclem8  34856  pmodN  36868  tgrpgrplem  37767  tendoplass  37801  tendoicl  37814  erngdvlem3  38008  dvhvaddass  38115  dib0  38182  dib1dim2  38186  diclspsn  38212  cdlemn8  38222  dihopelvalcpre  38266  djhcom  38423  nn0expgcd  39064  kelac2  39545  mendbas  39664  mendsca  39669  mendring  39672  iscard4  39780  relexp01min  39938  relexpaddss  39943  iotain  40629  addrcom  40687  rnsnf  41324  itgsinexplem1  42119  volioc  42137  dirkertrigeqlem1  42264  fourierdlem104  42376  sqwvfoura  42394  sqwvfourb  42395  fzopredsuc  43404  fppr2odd  43743  efmndbas  43940  smndex1mndlem  43979  rngccatidALTV  44158  ringccatidALTV  44221  0dig2pr01  44568  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator