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

Theorem eqtr2d 2318
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1  |-  ( ph  ->  A  =  B )
eqtr2d.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eqtr2d  |-  ( ph  ->  C  =  A )

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 eqtr2d.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2eqtrd 2317 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2290 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625
This theorem is referenced by:  3eqtrrd  2322  3eqtr2rd  2324  ifan  3606  ifor  3607  dfopif  3795  onsucmin  4614  csbopeq1a  6175  oaabs2  6645  ecinxp  6736  resixpfo  6856  sbthlem3  6975  rankxpsuc  7554  fseqenlem2  7654  dfac2  7759  isf32lem9  7989  compsscnvlem  7998  ttukeylem7  8144  fpwwe2lem11  8264  00id  8989  submul2  9222  divadddiv  9477  infmsup  9734  fzval3  10913  ceim1l  10959  fldiv  10966  flmod  10987  intfrac  10988  modcyc2  11002  moddi  11009  uzrdgfni  11023  axdc4uzlem  11046  seqf1olem1  11087  seqf1olem2  11088  seqid2  11094  expnegz  11138  binom2sub  11222  binom3  11224  ccatco  11492  swrds2  11562  reim  11596  mulre  11608  addcj  11635  absimle  11796  clim2ser  12130  isercoll2  12144  serf0  12155  iseralt  12159  summolem3  12189  isumclim3  12224  fsumrev  12243  fsumshft  12244  fsum2mul  12253  incexc  12298  isumsplit  12301  mertenslem1  12342  ef4p  12395  tanval3  12416  efival  12434  sinmul  12454  bitsinvp1  12642  sadaddlem  12659  bitsshft  12668  smu01lem  12678  eulerthlem2  12852  pythagtriplem16  12885  pczpre  12902  pcqdiv  12912  pcadd  12939  pcfac  12949  prmreclem5  12969  4sqlem10  12996  4sqlem19  13012  vdwapun  13023  vdwlem1  13030  ramcl  13078  strfvd  13179  strfv2d  13180  xpsff1o  13472  xpslem  13477  2oppccomf  13630  oppcepi  13644  sscfn1  13696  sscfn2  13697  invfuc  13850  grpinvval2  14551  pgp0  14909  sylow1lem1  14911  sylow3lem2  14941  efgredleme  15054  efgcpbllemb  15066  frgpuptinv  15082  frgpup3lem  15088  gexexlem  15146  cyggenod  15173  gsumval3eu  15192  gsumval3  15193  gsumzaddlem  15205  dprd2db  15280  rnginvdv  15478  lss1d  15722  mplcoe3  16212  subrgascl  16241  ply1sclid  16365  znzrh2  16501  ipassr2  16553  ntrval2  16790  ordtuni  16922  cnclima  16999  cmpsub  17129  ptbasfi  17278  txbasval  17303  pt1hmeo  17499  alexsubALTlem1  17743  ressprdsds  17937  imasdsf1olem  17939  setsms  18028  tmsxms  18034  tmsxpsmopn  18085  subgnm  18151  tngnm  18169  tngngp2  18170  xrsxmet  18317  xrge0gsumle  18340  metdstri  18357  xrhmeo  18446  lebnumlem3  18463  pcorevlem  18526  pi1xfrcnvlem  18556  clmabs  18582  minveclem4a  18796  pjthlem1  18803  ovolunlem1a  18857  mbfres2  19002  i1faddlem  19050  ibladdlem  19176  iblabs  19185  ditgsplit  19213  dvnres  19282  dveflem  19328  dveq0  19349  dvfsumabs  19372  itgsubstlem  19397  evlseu  19402  ply1divex  19524  dgrco  19658  plycjlem  19659  taylthlem1  19754  pserdv2  19808  abelthlem6  19814  abelthlem7  19816  tangtx  19875  abssinper  19888  sineq0  19891  explog  19949  reexplog  19950  eflogeq  19957  tanarg  19972  logtayl  20009  logtayl2  20011  ang180lem3  20111  affineequiv  20125  affineequiv2  20126  chordthmlem4  20134  chordthmlem5  20135  dcubic1lem  20141  dcubic2  20142  dcubic  20144  mcubic  20145  cubic2  20146  dquartlem1  20149  dquart  20151  quart1lem  20153  quartlem1  20155  quart  20159  acoscos  20191  atanlogaddlem  20211  atantayl2  20236  atantayl3  20237  birthdaylem2  20249  efrlim  20266  amgmlem  20286  logdifbnd  20290  emcllem3  20293  emcllem6  20296  basellem3  20322  basellem8  20327  basellem9  20328  chtprm  20393  logfaclbnd  20463  perfect1  20469  bcp1ctr  20520  bclbnd  20521  bposlem1  20525  lgsdilem  20563  lgsdirnn0  20580  lgsdinn0  20581  lgseisenlem2  20591  lgsquadlem1  20595  2sqlem2  20605  mul2sq  20606  vmadivsum  20633  rpvmasumlem  20638  dchrisumlem1  20640  dchrisumlem2  20641  dchrmusum2  20645  dchrvmasum2if  20648  dchrisum0lem2  20669  logsqvma2  20694  selberg3  20710  selberg4lem1  20711  pntrsumo1  20716  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem5  20732  pntibndlem2  20742  pntlemk  20757  pntlemo  20758  ostth2lem4  20787  ostth3  20789  grpoidinvlem2  20874  gxid  20942  subgores  20973  nvmtri  21239  cnnvm  21253  nvnd  21259  ipidsq  21288  ipnm  21289  ipipcj  21293  blocnilem  21384  ipasslem2  21412  dipsubdir  21428  hvaddsubval  21614  pjhthlem1  21972  pjspansn  22158  pjo  22252  unoplin  22502  adjadj  22518  hmoplin  22524  eigvec1  22544  lnopeqi  22590  nmcexi  22608  lnfnsubi  22628  riesz3i  22644  kbass6  22703  leoprf2  22709  leoprf  22710  pjnmopi  22730  mdslmd1lem1  22907  mdslmd1lem2  22908  superpos  22936  ballotlemfp1  23052  xlt2addrd  23255  mndpluscn  23301  xrge0tsmseq  23386  esumcst  23438  esumpcvgval  23448  probdif  23625  derangen2  23707  subfaclefac  23709  subfaclim  23721  sinccvglem  24007  brbtwn2  24535  colinearalglem4  24539  axsegconlem1  24547  axpaschlem  24570  axcontlem4  24597  axcontlem7  24600  axcontlem8  24601  ltflcei  24930  svs3  25499  2wsms  25619  lvsovso  25637  idsubfun  25869  morexcmp  25978  lineval42  26091  filnetlem4  26341  sdclem2  26463  ismtycnv  26537  heiborlem10  26555  mzpsubmpt  26832  irrapxlem3  26920  pellexlem6  26930  pell1234qrne0  26949  pell1234qrreccl  26950  pell1234qrmulcl  26951  pell14qrdich  26965  pell1qrgaplem  26969  rmxluc  27032  rmyluc  27033  jm2.24nn  27057  jm2.18  27092  jm2.19lem2  27094  jm2.19lem3  27095  jm2.22  27099  jm2.23  27100  jm2.16nn0  27108  jm2.27c  27111  fnwe2lem2  27159  lmhmfgsplit  27195  pwssplit1  27199  dsmmfi  27215  frlmlss  27230  frlmlbs  27260  frlmup3  27263  islindf4  27319  hbtlem2  27339  psgnunilem1  27427  psgnuni  27433  hashgcdeq  27528  dvconstbi  27562  fmuldfeqlem1  27723  stoweidlem22  27782  stoweidlem32  27792  sigarcol  27865  recsec  28237  reccsc  28238  bnj1415  29141  lflvsass  29344  lkrscss  29361  eqlkr  29362  eqlkr3  29364  ldualvsdi2  29407  omllaw3  29508  cmtcomlemN  29511  cmtbr3N  29517  omlfh3N  29522  llnexchb2lem  30130  dalawlem7  30139  dalawlem11  30143  dalawlem12  30144  pol1N  30172  paddatclN  30211  4atexlemcnd  30334  ltrncoidN  30390  cdleme3b  30491  cdleme11  30532  cdleme15a  30536  cdleme22e  30606  cdleme22eALTN  30607  cdleme22g  30610  cdlemg18b  30941  trlcoat  30985  cdlemk2  31094  cdlemk4  31096  cdlemki  31103  cdlemksv2  31109  cdlemk15  31117  cdlemk55a  31221  diainN  31320  dia2dimlem3  31329  dia2dimlem5  31331  dvhlveclem  31371  diaocN  31388  cdlemn4  31461  cdlemn8  31467  dihopelvalcpre  31511  dihmeetlem9N  31578  dih1dimatlem  31592  dihpN  31599  dochvalr3  31626  dochsat  31646  djhjlj  31666  dochdmm1  31673  dihjatcclem4  31684  dihjat1  31692  dihjat4  31696  dochsnkr2cl  31737  dochfl1  31739  lclkrlem2j  31779  mapdordlem2  31900  mapdrvallem2  31908  hdmap10  32106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-cleq 2278
  Copyright terms: Public domain W3C validator