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

Theorem 3eqtr4a 2489
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  |-  A  =  B
3eqtr4a.2  |-  ( ph  ->  C  =  A )
3eqtr4a.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4a  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3  |-  ( ph  ->  C  =  A )
2 3eqtr4a.1 . . 3  |-  A  =  B
31, 2syl6eq 2479 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2466 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-cleq 2414
This theorem is referenced by:  rabsnif  4069  uniintsn  4293  iinvdif  4371  iununi  4387  dmxpid  5073  rnxpid  5289  csbrn  5316  dmsnsnsn  5333  opswap  5342  xpcoid  5396  unizlim  5558  fvco4i  5959  fndmdifcom  6002  fmptsng  6100  fmptsnd  6101  csbov  6340  ordunisuc  6673  offres  6802  1stval2  6824  2ndval2  6825  cnvf1olem  6905  fparlem3  6909  fparlem4  6910  imacosupp  6966  seqomlem1  7178  ecovcom  7480  ecovass  7481  ecovdi  7482  resixpfo  7571  mapunen  7750  cardidm  8401  cardiun  8424  alephcard  8508  cardalephex  8528  cardcf  8689  cfidm  8712  alephsing  8713  itunisuc  8856  itunitc  8858  ituniiun  8859  alephadd  9009  alephreg  9014  pwcfsdom  9015  addcompq  9382  addcomnq  9383  mulcompq  9384  mulcomnq  9385  addassnq  9390  mulassnq  9391  addid1  9820  zeo  11028  xnegneg  11514  xaddcom  11538  xaddid1  11539  xnegdi  11541  xmulid1  11572  xadddilem  11587  ixxin  11659  fzsuc2  11860  expneg  12286  sq01  12400  facp1  12470  bcpasc  12512  hashf1lem1  12622  hashf1  12624  swrdccatin1  12841  swrdccat3blem  12853  repswsymballbi  12885  cshwmodn  12899  repswcshw  12913  trclun  13078  relexpcnv  13098  absexp  13367  sqreulem  13422  fsumf1o  13788  fsumadd  13804  fsumrev2  13842  fsumparts  13865  fsumrelem  13866  fprodf1o  13999  fprodmul  14013  fproddiv  14014  fprodfac  14026  fallfacfwd  14088  efexp  14154  tanval2  14186  sqr2irrlem  14299  sadeq  14445  smumullem  14465  smumul  14466  gcdcom  14483  gcd0id  14486  gcdass  14512  lcmcom  14556  lcmneg  14567  lcmass  14578  nn0gcdsq  14700  dfphi2  14721  pcneg  14822  setscom  15152  strfvi  15162  setsnid  15164  ressbas  15178  ressinbas  15184  ressress  15186  firest  15330  topnval  15332  xpsfeq  15469  xpsaddlem  15480  xpsvsca  15484  homffval  15594  oppchomfval  15618  oppcbas  15622  rescbas  15733  rescco  15736  cofuass  15793  fucbas  15864  fuchom  15865  setccatid  15978  estrccatid  16016  xpcbas  16062  xpchomfval  16063  xpccofval  16066  oduleval  16376  oduglb  16384  odulub  16386  ipotset  16402  grpinvfvi  16706  cntrval  16972  cntzval  16974  oppgplusfval  16998  symgbas  17020  symggrp  17040  pmtrprfval  17127  m1expaddsub  17138  sylow1lem2  17250  sylow3lem1  17278  oppglsm  17293  gsumzsplit  17559  gsum2dlem2  17602  gsumcom2  17606  dprd2dlem2  17672  dprd2da  17674  dmdprdsplit2lem  17677  mgpplusg  17726  mgpress  17733  ringidval  17736  opprmulfval  17852  abvtrivd  18067  sralem  18399  srasca  18403  sravsca  18404  sraip  18405  rlmval  18413  psrmulr  18607  mplmonmul  18687  mplcoe3  18689  opsrbaslem  18700  opsrtoslem2  18707  psr1val  18778  ply1basfvi  18833  ply1plusgfvi  18834  psr1sca2  18843  evl1fval1lem  18917  zlmlem  19086  zlmsca  19090  zlmvsca  19091  psgninv  19148  ocvval  19228  thlbas  19257  thlle  19258  thloc  19260  dsmmval2  19297  mattpos1  19479  mdettpos  19634  smadiadetglem1  19694  tgdif0  20006  indislem  20013  restco  20178  txtopon  20604  txindislem  20646  qtopres  20711  hmphindis  20810  ptuncnv  20820  snclseqg  21128  tsmssplit  21164  ussval  21272  tuslem  21280  setsmsbas  21488  tnglem  21646  tngds  21654  tngtset  21655  pcoass  22053  cphsqrtcl2  22162  rrxcph  22349  ovolunlem1a  22447  ioorinv  22526  ioorinvOLD  22531  itg11  22647  itg1mulc  22660  itg2cnlem1  22717  iblss2  22761  ibladdlem  22775  itgfsum  22782  iblabslem  22783  iblabs  22784  ditgneg  22810  deg1fvi  23032  dgrco  23227  logfac  23548  cxpexp  23611  cxpmul2  23632  cxpsqrt  23646  dvcxp1  23678  dvcxp2  23679  ang180lem1  23736  mcubic  23771  quart1  23780  reasinsin  23820  atanlogaddlem  23837  atantayl2  23862  log2tlbnd  23869  basellem2  24006  basellem3  24007  basellem5  24009  basellem8  24012  dchrmulid2  24178  bcp1ctr  24205  lgsneg  24245  lgsneg1  24246  lgsdir2  24254  lgsdir  24256  lgsdi  24258  lgsquad2lem2  24285  pntleml  24447  motgrp  24586  lmiisolem  24836  ttglem  24904  eupath2lem3  25705  bafval  26221  ipidsq  26347  ipasslem1  26470  pjclem2  27847  cvmdi  27975  imadifxp  28214  iundisjcnt  28380  resvsca  28601  indval2  28844  bayesth  29280  plymulx  29445  subfacp1lem6  29916  mvtval  30146  mexval  30148  mexval2  30149  mdvval  30150  mrsubfval  30154  mrsubvrs  30168  msubfval  30170  elmsubrn  30174  mvhfval  30179  mpstval  30181  msrfval  30183  mstaval  30190  mthmval  30221  bccolsum  30382  dfrdg2  30449  dfrdg3  30450  dfrdg4  30723  ordtoplem  31100  ordcmp  31112  poimirlem6  31910  poimirlem7  31911  poimirlem11  31915  poimirlem12  31916  poimirlem13  31917  poimirlem14  31918  poimirlem16  31920  poimirlem19  31923  poimirlem21  31925  poimirlem22  31926  poimirlem27  31931  poimirlem31  31935  poimirlem32  31936  mblfinlem2  31942  itg2addnclem2  31958  ibladdnclem  31962  iblabsnclem  31969  iblabsnc  31970  iblmulc2nc  31971  ftc1anclem8  31988  pmodN  33384  tgrpgrplem  34285  tendoplass  34319  tendoicl  34332  erngdvlem3  34526  dvhvaddass  34634  dib0  34701  dib1dim2  34705  diclspsn  34731  cdlemn8  34741  dihopelvalcpre  34785  djhcom  34942  kelac2  35893  mendbas  36020  mendsca  36025  mendring  36028  relexp01min  36275  relexpaddss  36280  iotain  36738  addrcom  36798  itgsinexplem1  37770  volioc  37789  dirkertrigeqlem1  37900  fourierdlem104  38014  sqwvfoura  38032  sqwvfourb  38033  fzopredsuc  38590  opidg  38863  egrsubgr  39123  0uhgrsubgr  39125  rngccatidALTV  39611  ringccatidALTV  39674  0dig2pr01  40043  nn0sumshdiglemB  40053  dpfrac1  40114
  Copyright terms: Public domain W3C validator