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

Theorem eqtr2d 2317
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 2316 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2289 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  3eqtrrd  2321  3eqtr2rd  2323  ifan  3605  ifor  3606  dfopif  3794  onsucmin  4611  csbopeq1a  6135  oaabs2  6639  ecinxp  6730  resixpfo  6850  sbthlem3  6969  rankxpsuc  7548  fseqenlem2  7648  dfac2  7753  isf32lem9  7983  compsscnvlem  7992  ttukeylem7  8138  fpwwe2lem11  8258  00id  8983  submul2  9216  divadddiv  9471  infmsup  9728  fzval3  10907  ceim1l  10953  fldiv  10960  flmod  10981  intfrac  10982  modcyc2  10996  moddi  11003  uzrdgfni  11017  axdc4uzlem  11040  seqf1olem1  11081  seqf1olem2  11082  seqid2  11088  expnegz  11132  binom2sub  11216  binom3  11218  ccatco  11486  swrds2  11556  reim  11590  mulre  11602  addcj  11629  absimle  11790  clim2ser  12124  isercoll2  12138  serf0  12149  iseralt  12153  summolem3  12183  isumclim3  12218  fsumrev  12237  fsumshft  12238  fsum2mul  12247  incexc  12292  isumsplit  12295  mertenslem1  12336  ef4p  12389  tanval3  12410  efival  12428  sinmul  12448  bitsinvp1  12636  sadaddlem  12653  bitsshft  12662  smu01lem  12672  eulerthlem2  12846  pythagtriplem16  12879  pczpre  12896  pcqdiv  12906  pcadd  12933  pcfac  12943  prmreclem5  12963  4sqlem10  12990  4sqlem19  13006  vdwapun  13017  vdwlem1  13024  ramcl  13072  strfvd  13173  strfv2d  13174  xpsff1o  13466  xpslem  13471  2oppccomf  13624  oppcepi  13638  sscfn1  13690  sscfn2  13691  invfuc  13844  grpinvval2  14545  pgp0  14903  sylow1lem1  14905  sylow3lem2  14935  efgredleme  15048  efgcpbllemb  15060  frgpuptinv  15076  frgpup3lem  15082  gexexlem  15140  cyggenod  15167  gsumval3eu  15186  gsumval3  15187  gsumzaddlem  15199  dprd2db  15274  rnginvdv  15472  lss1d  15716  mplcoe3  16206  subrgascl  16235  ply1sclid  16359  znzrh2  16495  ipassr2  16547  ntrval2  16784  ordtuni  16916  cnclima  16993  cmpsub  17123  ptbasfi  17272  txbasval  17297  pt1hmeo  17493  alexsubALTlem1  17737  ressprdsds  17931  imasdsf1olem  17933  setsms  18022  tmsxms  18028  tmsxpsmopn  18079  subgnm  18145  tngnm  18163  tngngp2  18164  xrsxmet  18311  xrge0gsumle  18334  metdstri  18351  xrhmeo  18440  lebnumlem3  18457  pcorevlem  18520  pi1xfrcnvlem  18550  clmabs  18576  minveclem4a  18790  pjthlem1  18797  ovolunlem1a  18851  mbfres2  18996  i1faddlem  19044  ibladdlem  19170  iblabs  19179  ditgsplit  19207  dvnres  19276  dveflem  19322  dveq0  19343  dvfsumabs  19366  itgsubstlem  19391  evlseu  19396  ply1divex  19518  dgrco  19652  plycjlem  19653  taylthlem1  19748  pserdv2  19802  abelthlem6  19808  abelthlem7  19810  tangtx  19869  abssinper  19882  sineq0  19885  explog  19943  reexplog  19944  eflogeq  19951  tanarg  19966  logtayl  20003  logtayl2  20005  ang180lem3  20105  affineequiv  20119  affineequiv2  20120  chordthmlem4  20128  chordthmlem5  20129  dcubic1lem  20135  dcubic2  20136  dcubic  20138  mcubic  20139  cubic2  20140  dquartlem1  20143  dquart  20145  quart1lem  20147  quartlem1  20149  quart  20153  acoscos  20185  atanlogaddlem  20205  atantayl2  20230  atantayl3  20231  birthdaylem2  20243  efrlim  20260  amgmlem  20280  logdifbnd  20284  emcllem3  20287  emcllem6  20290  basellem3  20316  basellem8  20321  basellem9  20322  chtprm  20387  logfaclbnd  20457  perfect1  20463  bcp1ctr  20514  bclbnd  20515  bposlem1  20519  lgsdilem  20557  lgsdirnn0  20574  lgsdinn0  20575  lgseisenlem2  20585  lgsquadlem1  20589  2sqlem2  20599  mul2sq  20600  vmadivsum  20627  rpvmasumlem  20632  dchrisumlem1  20634  dchrisumlem2  20635  dchrmusum2  20639  dchrvmasum2if  20642  dchrisum0lem2  20663  logsqvma2  20688  selberg3  20704  selberg4lem1  20705  pntrsumo1  20710  pntrlog2bndlem2  20723  pntrlog2bndlem3  20724  pntrlog2bndlem5  20726  pntibndlem2  20736  pntlemk  20751  pntlemo  20752  ostth2lem4  20781  ostth3  20783  grpoidinvlem2  20866  gxid  20934  subgores  20965  nvmtri  21231  cnnvm  21245  nvnd  21251  ipidsq  21280  ipnm  21281  ipipcj  21285  blocnilem  21376  ipasslem2  21404  dipsubdir  21420  hvaddsubval  21608  pjhthlem1  21966  pjspansn  22152  pjo  22246  unoplin  22496  adjadj  22512  hmoplin  22518  eigvec1  22538  lnopeqi  22584  nmcexi  22602  lnfnsubi  22622  riesz3i  22638  kbass6  22697  leoprf2  22703  leoprf  22704  pjnmopi  22724  mdslmd1lem1  22901  mdslmd1lem2  22902  superpos  22930  ballotlemfp1  23046  derangen2  23112  subfaclefac  23114  subfaclim  23126  sinccvglem  23412  brbtwn2  23943  colinearalglem4  23947  axsegconlem1  23955  axpaschlem  23978  axcontlem4  24005  axcontlem7  24008  axcontlem8  24009  svs3  24899  2wsms  25019  lvsovso  25037  idsubfun  25269  morexcmp  25378  lineval42  25491  filnetlem4  25741  sdclem2  25863  ismtycnv  25937  heiborlem10  25955  mzpsubmpt  26232  irrapxlem3  26320  pellexlem6  26330  pell1234qrne0  26349  pell1234qrreccl  26350  pell1234qrmulcl  26351  pell14qrdich  26365  pell1qrgaplem  26369  rmxluc  26432  rmyluc  26433  jm2.24nn  26457  jm2.18  26492  jm2.19lem2  26494  jm2.19lem3  26495  jm2.22  26499  jm2.23  26500  jm2.16nn0  26508  jm2.27c  26511  fnwe2lem2  26559  lmhmfgsplit  26595  pwssplit1  26599  dsmmfi  26615  frlmlss  26630  frlmlbs  26660  frlmup3  26663  islindf4  26719  hbtlem2  26739  psgnunilem1  26827  psgnuni  26833  hashgcdeq  26928  dvconstbi  26962  fmuldfeqlem1  27123  stoweidlem22  27182  stoweidlem32  27192  recsec  27498  reccsc  27499  bnj1415  28347  lflvsass  28550  lkrscss  28567  eqlkr  28568  eqlkr3  28570  ldualvsdi2  28613  omllaw3  28714  cmtcomlemN  28717  cmtbr3N  28723  omlfh3N  28728  llnexchb2lem  29336  dalawlem7  29345  dalawlem11  29349  dalawlem12  29350  pol1N  29378  paddatclN  29417  4atexlemcnd  29540  ltrncoidN  29596  cdleme3b  29697  cdleme11  29738  cdleme15a  29742  cdleme22e  29812  cdleme22eALTN  29813  cdleme22g  29816  cdlemg18b  30147  trlcoat  30191  cdlemk2  30300  cdlemk4  30302  cdlemki  30309  cdlemksv2  30315  cdlemk15  30323  cdlemk55a  30427  diainN  30526  dia2dimlem3  30535  dia2dimlem5  30537  dvhlveclem  30577  diaocN  30594  cdlemn4  30667  cdlemn8  30673  dihopelvalcpre  30717  dihmeetlem9N  30784  dih1dimatlem  30798  dihpN  30805  dochvalr3  30832  dochsat  30852  djhjlj  30872  dochdmm1  30879  dihjatcclem4  30890  dihjat1  30898  dihjat4  30902  dochsnkr2cl  30943  dochfl1  30945  lclkrlem2j  30985  mapdordlem2  31106  mapdrvallem2  31114  hdmap10  31312
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-cleq 2277
  Copyright terms: Public domain W3C validator