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

Theorem 3eqtr4a 2501
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 2491 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2478 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  rabsnif  3956  uniintsn  4177  iinvdif  4254  iununi  4267  unizlim  4847  dmxpid  5071  rnxpid  5283  csbrn  5311  dmsnsnsn  5329  opswap  5338  xpcoid  5390  fvco4i  5781  fndmdifcom  5820  fmptsng  5912  csbov  6135  ordunisuc  6455  offres  6584  1stval2  6606  2ndval2  6607  cnvf1olem  6682  fparlem3  6686  fparlem4  6687  imacosupp  6741  seqomlem1  6917  ecovcom  7223  ecovass  7224  ecovdi  7225  resixpfo  7313  mapunen  7492  cardidm  8141  cardiun  8164  alephcard  8252  cardalephex  8272  cardcf  8433  cfidm  8456  alephsing  8457  itunisuc  8600  itunitc  8602  ituniiun  8603  alephadd  8753  alephreg  8758  pwcfsdom  8759  addcompq  9131  addcomnq  9132  mulcompq  9133  mulcomnq  9134  addassnq  9139  mulassnq  9140  addid1  9561  zeo  10739  xnegneg  11196  xaddcom  11220  xaddid1  11221  xnegdi  11223  xmulid1  11254  xadddilem  11269  ixxin  11329  fzsuc2  11526  expneg  11885  sq01  11998  facp1  12068  bcpasc  12109  hashf1lem1  12220  hashf1  12222  eqs1  12312  swrdccatin1  12386  swrdccat3blem  12398  repswsymballbi  12430  cshwmodn  12444  repswcshw  12458  absexp  12805  sqreulem  12859  fsumf1o  13212  fsumadd  13227  fsumrev2  13261  fsumparts  13281  fsumrelem  13282  efexp  13397  tanval2  13429  sqr2irrlem  13542  sadeq  13680  smumullem  13700  smumul  13701  gcdcom  13716  gcd0id  13719  gcdass  13741  nn0gcdsq  13842  dfphi2  13861  pcneg  13952  setscom  14216  strfvi  14226  setsnid  14228  ressbas  14240  ressinbas  14246  ressress  14247  firest  14383  topnval  14385  xpsfeq  14514  xpsaddlem  14525  xpsvsca  14529  homffval  14642  oppchomfval  14665  oppcbas  14669  rescbas  14754  rescco  14757  cofuass  14811  fucbas  14882  fuchom  14883  setccatid  14964  xpcbas  15000  xpchomfval  15001  xpccofval  15004  oduleval  15313  oduglb  15321  odulub  15323  ipotset  15339  grpinvfvi  15591  cntrval  15849  cntzval  15851  oppgplusfval  15875  symgbas  15897  symggrp  15917  pmtrprfval  16005  m1expaddsub  16016  sylow1lem2  16110  sylow3lem1  16138  oppglsm  16153  gsumzsplit  16430  gsumzsplitOLD  16431  gsum2dlem2  16474  gsum2dOLD  16476  gsumcom2  16479  dprd2dlem2  16551  dprd2da  16553  dmdprdsplit2lem  16556  mgpplusg  16607  mgpress  16614  rngidval  16617  opprmulfval  16729  abvtrivd  16937  sralem  17270  srasca  17274  sravsca  17275  sraip  17276  rlmval  17284  psrmulr  17467  mplmonmul  17555  mplcoe3  17557  mplcoe3OLD  17558  opsrbaslem  17571  opsrtoslem2  17578  psr1val  17654  ply1basfvi  17708  ply1plusgfvi  17709  psr1sca2  17718  evl1fval1lem  17776  zlmlem  17960  zlmsca  17964  zlmvsca  17965  psgninv  18024  ocvval  18104  thlbas  18133  thlle  18134  thloc  18136  dsmmval2  18173  mattpos1  18352  mdettpos  18429  smadiadetglem1  18489  tgdif0  18609  indislem  18616  restco  18780  txtopon  19176  txindislem  19218  qtopres  19283  hmphindis  19382  ptuncnv  19392  snclseqg  19698  tsmssplit  19738  ussval  19846  tuslem  19854  setsmsbas  20062  tnglem  20238  tngds  20246  tngtset  20247  pcoass  20608  cphsqrcl2  20717  rrxcph  20908  ovolunlem1a  20991  ioorinv  21068  itg11  21181  itg1mulc  21194  itg2cnlem1  21251  iblss2  21295  ibladdlem  21309  itgfsum  21316  iblabslem  21317  iblabs  21318  ditgneg  21344  deg1fvi  21568  dgrco  21754  logfac  22061  cxpexp  22125  cxpmul2  22146  cxpsqr  22160  dvcxp2  22193  ang180lem1  22217  mcubic  22254  quart1  22263  reasinsin  22303  atanlogaddlem  22320  atantayl2  22345  log2tlbnd  22352  basellem2  22431  basellem3  22432  basellem5  22434  basellem8  22437  dchrmulid2  22603  bcp1ctr  22630  lgsneg  22670  lgsneg1  22671  lgsdir2  22679  lgsdir  22681  lgsdi  22683  lgsquad2lem2  22710  pntleml  22872  ttglem  23134  eupath2lem3  23612  bafval  23994  ipidsq  24120  ipasslem1  24243  pjclem2  25612  cvmdi  25740  imadifxp  25951  iundisjcnt  26094  resvsca  26310  indval2  26483  bayesth  26834  subfacp1lem6  27085  fprodf1o  27471  fprodmul  27483  fproddiv  27484  fprodfac  27495  fallfacfwd  27551  dfrdg2  27621  dfrdg3  27622  dfrdg4  27993  ordtoplem  28293  ordcmp  28305  mblfinlem2  28441  itg2addnclem2  28456  ibladdnclem  28460  iblabsnclem  28467  iblabsnc  28468  iblmulc2nc  28469  ftc1anclem8  28486  kelac2  29430  mendbas  29553  mendsca  29558  mendrng  29561  iotain  29683  addrcom  29743  itgsinexplem1  29806  fmptsnd  30734  dpfrac1  31119  pmodN  33506  tgrpgrplem  34405  tendoplass  34439  tendoicl  34452  erngdvlem3  34646  dvhvaddass  34754  dib0  34821  dib1dim2  34825  diclspsn  34851  cdlemn8  34861  dihopelvalcpre  34905  djhcom  35062
  Copyright terms: Public domain W3C validator