Theorem eqtr2d 2466

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

Step	Hyp	Ref	Expression
1		eqtr2d.1	. . 3 |- ( ph -> A = B )
2		eqtr2d.2	. . 3 |- ( ph -> B = C )
3	1, 2	eqtrd 2465	. 2 |- ( ph -> A = C )
4	3	eqcomd 2438	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426

This theorem is referenced by:  3eqtrrd  2470  3eqtr2rd  2472  ifan  3823  ifor  3824  dfopif  4044  nvocnv  5975  onsucmin  6421  csbopeq1a  6616  oaabs2  7072  ecinxp  7163  resixpfo  7289  sbthlem3  7411  rankxpsuc  8077  fseqenlem2  8183  dfac2  8288  isf32lem9  8518  compsscnvlem  8527  ttukeylem7  8672  fpwwe2lem11  8794  00id  9531  submul2  9772  divadddiv  10033  infmsup  10295  xadd4d  11253  fzval3  11588  fzoshftral  11619  ceim1l  11669  fldiv  11682  flmod  11705  intfrac  11706  modcyc2  11727  moddi  11749  uzrdgfni  11764  axdc4uzlem  11787  seqf1olem1  11828  seqf1olem2  11829  seqid2  11835  expnegz  11881  binom2sub  11966  binom3  11968  ccats1swrdeq  12346  swrdccatin12lem2  12363  swrdccatin12  12365  swrdccat3b  12370  cshweqrep  12438  ccatco  12446  swrds2  12528  reim  12581  mulre  12593  addcj  12620  absimle  12781  clim2ser  13115  isercoll2  13129  serf0  13141  iseralt  13145  summolem3  13174  isumclim3  13209  fsumrev  13228  fsumshft  13229  fsum2mul  13238  incexc  13282  isumsplit  13285  mertenslem1  13326  ef4p  13379  tanval3  13400  efival  13418  sinmul  13438  bitsinvp1  13627  sadaddlem  13644  bitsshft  13653  smu01lem  13663  eulerthlem2  13839  pythagtriplem16  13879  pczpre  13896  pcqdiv  13906  pcadd  13933  pcfac  13943  prmreclem5  13963  4sqlem10  13990  4sqlem19  14006  vdwapun  14017  vdwlem1  14024  ramcl  14072  strfvd  14187  strfv2d  14188  xpsff1o  14488  xpslem  14493  2oppccomf  14646  oppcepi  14660  sscfn1  14712  sscfn2  14713  invfuc  14866  grpinvssd  15582  grpinvval2  15588  pmtrdifwrdellem2  15967  psgnunilem1  15978  psgnuni  15984  pgp0  16074  sylow1lem1  16076  sylow3lem2  16106  efgredleme  16219  efgcpbllemb  16231  frgpuptinv  16247  frgpup3lem  16253  gexexlem  16313  cyggenod  16340  gsumval3eu  16360  gsumval3OLD  16361  gsumval3  16364  gsumzaddlem  16387  gsumzaddlemOLD  16389  dprd2db  16515  rnginvdv  16719  lss1d  16965  pwssplit1  17061  mplcoe3  17478  mplcoe3OLD  17479  subrgascl  17511  ply1sclid  17637  znzrh2  17819  regsumsupp  17893  ipassr2  17917  dsmmfi  18004  frlmlss  18017  frlmip  18044  frlmlbs  18066  frlmup3  18069  islindf4  18108  1marepvmarrepid  18227  madurid  18291  smadiadetlem3  18315  ntrval2  18496  ordtuni  18635  cnclima  18713  cmpsub  18844  ptbasfi  18995  txbasval  19020  pt1hmeo  19220  alexsubALTlem1  19460  trust  19645  ussid  19676  ressuss  19679  ressprdsds  19787  imasdsf1olem  19789  setsms  19896  tmsxms  19902  tmsxpsmopn  19953  subgnm  20060  tngnm  20078  tngngp2  20079  xrsxmet  20227  xrge0gsumle  20251  metdstri  20268  xrhmeo  20359  lebnumlem3  20376  pcorevlem  20439  pi1xfrcnvlem  20469  clmabs  20495  cvsmuleqdivd  20524  rrxip  20735  rrxds  20738  minveclem4a  20758  pjthlem1  20765  ovolunlem1a  20820  mbfres2  20964  i1faddlem  21012  ibladdlem  21138  iblabs  21147  ditgsplit  21177  dvnres  21246  dveflem  21292  dveq0  21313  dvfsumabs  21336  itgsubstlem  21361  evlseu  21367  ply1divex  21492  dgrco  21626  plycjlem  21627  taylthlem1  21722  pserdv2  21779  abelthlem6  21785  abelthlem7  21787  tangtx  21851  abssinper  21864  sineq0  21867  explog  21926  reexplog  21927  eflogeq  21934  abslogle  21951  tanarg  21952  logtayl  21989  logtayl2  21991  ang180lem3  22091  affineequiv  22105  affineequiv2  22106  chordthmlem4  22114  chordthmlem5  22115  heron  22117  dcubic1lem  22122  dcubic2  22123  dcubic  22125  mcubic  22126  cubic2  22127  dquartlem1  22130  dquart  22132  quart1lem  22134  quartlem1  22136  quart  22140  acoscos  22172  atanlogaddlem  22192  atantayl2  22217  atantayl3  22218  birthdaylem2  22230  efrlim  22247  amgmlem  22267  logdifbnd  22271  emcllem3  22275  emcllem6  22278  basellem3  22304  basellem8  22309  basellem9  22310  chtprm  22375  logfaclbnd  22445  perfect1  22451  bcp1ctr  22502  bclbnd  22503  bposlem1  22507  lgsdilem  22545  lgsdirnn0  22562  lgsdinn0  22563  lgseisenlem2  22573  lgsquadlem1  22577  2sqlem2  22587  mul2sq  22588  vmadivsum  22615  rpvmasumlem  22620  dchrisumlem1  22622  dchrisumlem2  22623  dchrmusum2  22627  dchrvmasum2if  22630  dchrisum0lem2  22651  logsqvma2  22676  selberg3  22692  selberg4lem1  22693  pntrsumo1  22698  pntrlog2bndlem2  22711  pntrlog2bndlem3  22712  pntrlog2bndlem5  22714  pntibndlem2  22724  pntlemk  22739  pntlemo  22740  ostth2lem4  22769  ostth3  22771  tgcgrextend  22820  tgbtwndiff  22840  tgifscgr  22841  trgcgrg  22847  tgidinside  22878  tgbtwnconn1lem1  22879  tgbtwnconn1lem2  22880  tgbtwnconn1lem3  22881  ismir  22928  miriso  22934  brbtwn2  22973  colinearalglem4  22977  axsegconlem1  22985  axpaschlem  23008  axcontlem4  23035  axcontlem7  23038  axcontlem8  23039  grpoidinvlem2  23514  gxid  23582  subgores  23613  nvmtri  23881  cnnvm  23895  nvnd  23901  ipidsq  23930  ipnm  23931  ipipcj  23935  blocnilem  24026  ipasslem2  24054  dipsubdir  24070  hvaddsubval  24257  pjhthlem1  24616  pjspansn  24802  pjo  24896  unoplin  25146  adjadj  25162  hmoplin  25168  eigvec1  25188  lnopeqi  25234  nmcexi  25252  lnfnsubi  25272  riesz3i  25288  kbass6  25347  leoprf2  25353  leoprf  25354  pjnmopi  25374  mdslmd1lem1  25551  mdslmd1lem2  25552  superpos  25580  fgreu  25813  resf1o  25854  xrge0tsmseq  26107  subrgchr  26114  rhmdvd  26141  pstmval  26175  mndpluscn  26209  qqhucn  26274  esumval  26353  gsumesum  26363  esumcst  26367  esumpcvgval  26380  oddpwdc  26584  eulerpartlemgvv  26606  sseqp1  26625  probdif  26650  ballotlemfp1  26721  sgnmul  26772  signsvtn  26832  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamgulmlem4  26865  lgamgulmlem5  26866  gamigam  26886  lgamcvg2  26888  gamfac  26900  derangen2  26909  subfaclefac  26911  subfaclim  26923  sinccvglem  27163  fprodshft  27333  fprodrev  27334  iprodclim3  27346  binomfallfaclem2  27389  ltflcei  28260  mblfinlem4  28272  ibladdnclem  28289  iblabsnc  28297  iblmulc2nc  28298  ftc1anclem6  28313  ftc1anclem8  28315  filnetlem4  28443  sdclem2  28479  ismtycnv  28542  heiborlem10  28560  mzpsubmpt  28921  irrapxlem3  29007  pellexlem6  29017  pell1234qrne0  29036  pell1234qrreccl  29037  pell1234qrmulcl  29038  pell14qrdich  29052  pell1qrgaplem  29056  rmxluc  29119  rmyluc  29120  jm2.24nn  29144  jm2.18  29179  jm2.19lem2  29181  jm2.19lem3  29182  jm2.22  29186  jm2.23  29187  jm2.16nn0  29195  jm2.27c  29198  fnwe2lem2  29246  lmhmfgsplit  29281  hbtlem2  29322  hashgcdeq  29408  dvconstbi  29450  stoweidlem22  29660  stoweidlem32  29670  wallispilem5  29707  stirlinglem5  29716  sigarcol  29743  elovmpt3rab1  30006  mulsubfacd  30015  powm2modprm  30091  wwlkextwrd  30203  clwwlkn2  30281  clwlkisclwwlklem2a3  30286  clwlkisclwwlk2  30295  clwwlkel  30298  clwwlkfo  30302  clwwlkext2edg  30307  wwlkext2clwwlk  30308  cshwlemma1  30332  frg2woteq  30496  extwwlkfablem1  30510  clwwlkextfrlem1  30512  numclwlk1lem2foa  30527  numclwlk1lem2fo  30531  numclwlk2lem2f  30539  lincext3  30696  lincresunit3  30721  recsec  30797  reccsc  30798  bnj1415  31728  lflvsass  32296  lkrscss  32313  eqlkr  32314  eqlkr3  32316  ldualvsdi2  32359  omllaw3  32460  cmtcomlemN  32463  cmtbr3N  32469  omlfh3N  32474  llnexchb2lem  33082  dalawlem7  33091  dalawlem11  33095  dalawlem12  33096  pol1N  33124  paddatclN  33163  4atexlemcnd  33286  ltrncoidN  33342  cdleme3b  33443  cdleme11  33484  cdleme15a  33488  cdleme22e  33558  cdleme22g  33562  cdlemg18b  33893  trlcoat  33937  cdlemk2  34046  cdlemk4  34048  cdlemki  34055  cdlemksv2  34061  cdlemk15  34069  cdlemk55a  34173  diainN  34272  dia2dimlem3  34281  dia2dimlem5  34283  dvhlveclem  34323  diaocN  34340  cdlemn4  34413  cdlemn8  34419  dihopelvalcpre  34463  dihmeetlem9N  34530  dih1dimatlem  34544  dihpN  34551  dochvalr3  34578  dochsat  34598  djhjlj  34618  dochdmm1  34625  dihjatcclem4  34636  dihjat1  34644  dihjat4  34648  dochsnkr2cl  34689  dochfl1  34691  lclkrlem2j  34731  mapdordlem2  34852  mapdrvallem2  34860  hdmap10  35058