Theorem eqtr2d 2493

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 2492	. 2 |- ( ph -> A = C )
4	3	eqcomd 2459	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-cleq 2443

This theorem is referenced by:  3eqtrrd  2497  3eqtr2rd  2499  ifan  3933  ifor  3934  dfopif  4154  nvocnv  6087  onsucmin  6532  csbopeq1a  6727  oaabs2  7184  ecinxp  7275  resixpfo  7401  sbthlem3  7523  rankxpsuc  8190  fseqenlem2  8296  dfac2  8401  isf32lem9  8631  compsscnvlem  8640  ttukeylem7  8785  fpwwe2lem11  8908  00id  9645  submul2  9886  divadddiv  10147  infmsup  10409  xadd4d  11367  fzdifsuc  11617  fzval3  11706  fzoshftral  11737  ceim1l  11787  fldiv  11800  flmod  11823  intfrac  11824  modcyc2  11845  moddi  11867  uzrdgfni  11882  axdc4uzlem  11905  seqf1olem1  11946  seqf1olem2  11947  seqid2  11953  expnegz  11999  binom2sub  12084  binom3  12086  ccats1swrdeq  12465  swrdccatin12lem2  12482  swrdccatin12  12484  swrdccat3b  12489  cshweqrep  12557  ccatco  12565  swrds2  12647  reim  12700  mulre  12712  addcj  12739  absimle  12900  clim2ser  13234  isercoll2  13248  serf0  13260  iseralt  13264  summolem3  13293  isumclim3  13328  mptfzshft  13347  fsumrev  13348  fsum2mul  13358  incexc  13402  isumsplit  13405  mertenslem1  13446  ef4p  13499  tanval3  13520  efival  13538  sinmul  13558  bitsinvp1  13747  sadaddlem  13764  bitsshft  13773  smu01lem  13783  eulerthlem2  13959  pythagtriplem16  13999  pczpre  14016  pcqdiv  14026  pcadd  14053  pcfac  14063  prmreclem5  14083  4sqlem10  14110  4sqlem19  14126  vdwapun  14137  vdwlem1  14144  ramcl  14192  strfvd  14307  strfv2d  14308  xpsff1o  14608  xpslem  14613  2oppccomf  14766  oppcepi  14780  sscfn1  14832  sscfn2  14833  invfuc  14986  grpinvssd  15705  grpinvval2  15711  pmtrdifwrdellem2  16090  psgnunilem1  16101  psgnuni  16107  pgp0  16199  sylow1lem1  16201  sylow3lem2  16231  efgredleme  16344  efgcpbllemb  16356  frgpuptinv  16372  frgpup3lem  16378  gexexlem  16438  cyggenod  16465  gsumval3eu  16485  gsumval3OLD  16486  gsumval3  16489  gsumzaddlem  16512  gsumzaddlemOLD  16514  dprd2db  16647  rnginvdv  16892  lss1d  17150  pwssplit1  17246  mplcoe3  17652  mplcoe3OLD  17653  subrgascl  17687  evlseu  17709  ply1sclid  17849  znzrh2  18087  regsumsupp  18161  ipassr2  18185  dsmmfi  18272  frlmlss  18285  frlmip  18312  frlmlbs  18334  frlmup3  18337  islindf4  18376  1marepvmarrepid  18497  madurid  18566  smadiadetlem3  18590  ntrval2  18771  ordtuni  18910  cnclima  18988  cmpsub  19119  ptbasfi  19270  txbasval  19295  pt1hmeo  19495  alexsubALTlem1  19735  trust  19920  ussid  19951  ressuss  19954  ressprdsds  20062  imasdsf1olem  20064  setsms  20171  tmsxms  20177  tmsxpsmopn  20228  subgnm  20335  tngnm  20353  tngngp2  20354  xrsxmet  20502  xrge0gsumle  20526  metdstri  20543  xrhmeo  20634  lebnumlem3  20651  pcorevlem  20714  pi1xfrcnvlem  20744  clmabs  20770  cvsmuleqdivd  20799  rrxip  21010  rrxds  21013  minveclem4a  21033  pjthlem1  21040  ovolunlem1a  21095  mbfres2  21239  i1faddlem  21287  ibladdlem  21413  iblabs  21422  ditgsplit  21452  dvnres  21521  dveflem  21567  dveq0  21588  dvfsumabs  21611  itgsubstlem  21636  ply1divex  21724  dgrco  21858  plycjlem  21859  taylthlem1  21954  pserdv2  22011  abelthlem6  22017  abelthlem7  22019  tangtx  22083  abssinper  22096  sineq0  22099  explog  22158  reexplog  22159  eflogeq  22166  abslogle  22183  tanarg  22184  logtayl  22221  logtayl2  22223  ang180lem3  22323  affineequiv  22337  affineequiv2  22338  chordthmlem4  22346  chordthmlem5  22347  heron  22349  dcubic1lem  22354  dcubic2  22355  dcubic  22357  mcubic  22358  cubic2  22359  dquartlem1  22362  dquart  22364  quart1lem  22366  quartlem1  22368  quart  22372  acoscos  22404  atanlogaddlem  22424  atantayl2  22449  atantayl3  22450  birthdaylem2  22462  efrlim  22479  amgmlem  22499  logdifbnd  22503  emcllem3  22507  emcllem6  22510  basellem3  22536  basellem8  22541  basellem9  22542  chtprm  22607  logfaclbnd  22677  perfect1  22683  bcp1ctr  22734  bclbnd  22735  bposlem1  22739  lgsdilem  22777  lgsdirnn0  22794  lgsdinn0  22795  lgseisenlem2  22805  lgsquadlem1  22809  2sqlem2  22819  mul2sq  22820  vmadivsum  22847  rpvmasumlem  22852  dchrisumlem1  22854  dchrisumlem2  22855  dchrmusum2  22859  dchrvmasum2if  22862  dchrisum0lem2  22883  logsqvma2  22908  selberg3  22924  selberg4lem1  22925  pntrsumo1  22930  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem5  22946  pntibndlem2  22956  pntlemk  22971  pntlemo  22972  ostth2lem4  23001  ostth3  23003  tgcgrextend  23056  tgbtwndiff  23077  tgifscgr  23080  trgcgrg  23086  tgidinside  23123  tgbtwnconn1lem1  23124  tgbtwnconn1lem2  23125  tgbtwnconn1lem3  23126  ismir  23189  miriso  23199  krippenlem  23210  midexlem  23212  ragmir  23220  footex  23237  colperplem3  23242  mideulem  23244  mideu  23245  brbtwn2  23286  colinearalglem4  23290  axsegconlem1  23298  axpaschlem  23321  axcontlem4  23348  axcontlem7  23351  axcontlem8  23352  grpoidinvlem2  23827  gxid  23895  subgores  23926  nvmtri  24194  cnnvm  24208  nvnd  24214  ipidsq  24243  ipnm  24244  ipipcj  24248  blocnilem  24339  ipasslem2  24367  dipsubdir  24383  hvaddsubval  24570  pjhthlem1  24929  pjspansn  25115  pjo  25209  unoplin  25459  adjadj  25475  hmoplin  25481  eigvec1  25501  lnopeqi  25547  nmcexi  25565  lnfnsubi  25585  riesz3i  25601  kbass6  25660  leoprf2  25666  leoprf  25667  pjnmopi  25687  mdslmd1lem1  25864  mdslmd1lem2  25865  superpos  25893  fgreu  26124  resf1o  26164  xrge0tsmseq  26389  subrgchr  26396  rhmdvd  26423  pstmval  26456  mndpluscn  26490  qqhucn  26555  esumval  26634  gsumesum  26644  esumcst  26648  esumpcvgval  26661  oddpwdc  26871  eulerpartlemgvv  26893  sseqp1  26912  probdif  26937  ballotlemfp1  27008  sgnmul  27059  signsvtn  27119  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem4  27152  lgamgulmlem5  27153  gamigam  27173  lgamcvg2  27175  gamfac  27187  derangen2  27196  subfaclefac  27198  subfaclim  27210  sinccvglem  27451  fprodshft  27621  fprodrev  27622  iprodclim3  27634  binomfallfaclem2  27677  ltflcei  28557  mblfinlem4  28569  ibladdnclem  28586  iblabsnc  28594  iblmulc2nc  28595  ftc1anclem6  28610  ftc1anclem8  28612  filnetlem4  28740  sdclem2  28776  ismtycnv  28839  heiborlem10  28857  mzpsubmpt  29217  irrapxlem3  29303  pellexlem6  29313  pell1234qrne0  29332  pell1234qrreccl  29333  pell1234qrmulcl  29334  pell14qrdich  29348  pell1qrgaplem  29352  rmxluc  29415  rmyluc  29416  jm2.24nn  29440  jm2.18  29475  jm2.19lem2  29477  jm2.19lem3  29478  jm2.22  29482  jm2.23  29483  jm2.16nn0  29491  jm2.27c  29494  fnwe2lem2  29542  lmhmfgsplit  29577  hbtlem2  29618  hashgcdeq  29704  dvconstbi  29746  stoweidlem22  29955  stoweidlem32  29965  wallispilem5  30002  stirlinglem5  30011  sigarcol  30038  elovmpt3rab1  30301  mulsubfacd  30310  powm2modprm  30386  wwlkextwrd  30498  clwwlkn2  30576  clwlkisclwwlklem2a3  30581  clwlkisclwwlk2  30590  clwwlkel  30593  clwwlkfo  30597  clwwlkext2edg  30602  wwlkext2clwwlk  30603  cshwlemma1  30627  frg2woteq  30791  extwwlkfablem1  30805  clwwlkextfrlem1  30807  numclwlk1lem2foa  30822  numclwlk1lem2fo  30826  numclwlk2lem2f  30834  lincext3  31097  lincresunit3  31122  mat2pmatghm  31193  pmatcollpwscmatlem1  31245  pmattomply1mhmlem2  31274  cpmadurid  31321  cpmidgsumm2pm  31323  cayhamlem2  31339  recsec  31387  reccsc  31388  bnj1415  32329  lflvsass  33032  lkrscss  33049  eqlkr  33050  eqlkr3  33052  ldualvsdi2  33095  omllaw3  33196  cmtcomlemN  33199  cmtbr3N  33205  omlfh3N  33210  llnexchb2lem  33818  dalawlem7  33827  dalawlem11  33831  dalawlem12  33832  pol1N  33860  paddatclN  33899  4atexlemcnd  34022  ltrncoidN  34078  cdleme3b  34179  cdleme11  34220  cdleme15a  34224  cdleme22e  34294  cdleme22g  34298  cdlemg18b  34629  trlcoat  34673  cdlemk2  34782  cdlemk4  34784  cdlemki  34791  cdlemksv2  34797  cdlemk15  34805  cdlemk55a  34909  diainN  35008  dia2dimlem3  35017  dia2dimlem5  35019  dvhlveclem  35059  diaocN  35076  cdlemn4  35149  cdlemn8  35155  dihopelvalcpre  35199  dihmeetlem9N  35266  dih1dimatlem  35280  dihpN  35287  dochvalr3  35314  dochsat  35334  djhjlj  35354  dochdmm1  35361  dihjatcclem4  35372  dihjat1  35380  dihjat4  35384  dochsnkr2cl  35425  dochfl1  35427  lclkrlem2j  35467  mapdordlem2  35588  mapdrvallem2  35596  hdmap10  35794