Theorem eqtr2d 2471

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

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 2419

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431

This theorem is referenced by:  3eqtrrd  2475  3eqtr2rd  2477  ifan  3830  ifor  3831  dfopif  4051  nvocnv  5983  onsucmin  6427  csbopeq1a  6622  oaabs2  7076  ecinxp  7167  resixpfo  7293  sbthlem3  7415  rankxpsuc  8081  fseqenlem2  8187  dfac2  8292  isf32lem9  8522  compsscnvlem  8531  ttukeylem7  8676  fpwwe2lem11  8799  00id  9536  submul2  9777  divadddiv  10038  infmsup  10300  xadd4d  11258  fzdifsuc  11508  fzval3  11597  fzoshftral  11628  ceim1l  11678  fldiv  11691  flmod  11714  intfrac  11715  modcyc2  11736  moddi  11758  uzrdgfni  11773  axdc4uzlem  11796  seqf1olem1  11837  seqf1olem2  11838  seqid2  11844  expnegz  11890  binom2sub  11975  binom3  11977  ccats1swrdeq  12355  swrdccatin12lem2  12372  swrdccatin12  12374  swrdccat3b  12379  cshweqrep  12447  ccatco  12455  swrds2  12537  reim  12590  mulre  12602  addcj  12629  absimle  12790  clim2ser  13124  isercoll2  13138  serf0  13150  iseralt  13154  summolem3  13183  isumclim3  13218  mptfzshft  13237  fsumrev  13238  fsum2mul  13248  incexc  13292  isumsplit  13295  mertenslem1  13336  ef4p  13389  tanval3  13410  efival  13428  sinmul  13448  bitsinvp1  13637  sadaddlem  13654  bitsshft  13663  smu01lem  13673  eulerthlem2  13849  pythagtriplem16  13889  pczpre  13906  pcqdiv  13916  pcadd  13943  pcfac  13953  prmreclem5  13973  4sqlem10  14000  4sqlem19  14016  vdwapun  14027  vdwlem1  14034  ramcl  14082  strfvd  14197  strfv2d  14198  xpsff1o  14498  xpslem  14503  2oppccomf  14656  oppcepi  14670  sscfn1  14722  sscfn2  14723  invfuc  14876  grpinvssd  15594  grpinvval2  15600  pmtrdifwrdellem2  15979  psgnunilem1  15990  psgnuni  15996  pgp0  16086  sylow1lem1  16088  sylow3lem2  16118  efgredleme  16231  efgcpbllemb  16243  frgpuptinv  16259  frgpup3lem  16265  gexexlem  16325  cyggenod  16352  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzaddlem  16399  gsumzaddlemOLD  16401  dprd2db  16532  rnginvdv  16776  lss1d  17024  pwssplit1  17120  mplcoe3  17525  mplcoe3OLD  17526  subrgascl  17560  evlseu  17582  ply1sclid  17720  znzrh2  17958  regsumsupp  18032  ipassr2  18056  dsmmfi  18143  frlmlss  18156  frlmip  18183  frlmlbs  18205  frlmup3  18208  islindf4  18247  1marepvmarrepid  18366  madurid  18430  smadiadetlem3  18454  ntrval2  18635  ordtuni  18774  cnclima  18852  cmpsub  18983  ptbasfi  19134  txbasval  19159  pt1hmeo  19359  alexsubALTlem1  19599  trust  19784  ussid  19815  ressuss  19818  ressprdsds  19926  imasdsf1olem  19928  setsms  20035  tmsxms  20041  tmsxpsmopn  20092  subgnm  20199  tngnm  20217  tngngp2  20218  xrsxmet  20366  xrge0gsumle  20390  metdstri  20407  xrhmeo  20498  lebnumlem3  20515  pcorevlem  20578  pi1xfrcnvlem  20608  clmabs  20634  cvsmuleqdivd  20663  rrxip  20874  rrxds  20877  minveclem4a  20897  pjthlem1  20904  ovolunlem1a  20959  mbfres2  21103  i1faddlem  21151  ibladdlem  21277  iblabs  21286  ditgsplit  21316  dvnres  21385  dveflem  21431  dveq0  21452  dvfsumabs  21475  itgsubstlem  21500  ply1divex  21588  dgrco  21722  plycjlem  21723  taylthlem1  21818  pserdv2  21875  abelthlem6  21881  abelthlem7  21883  tangtx  21947  abssinper  21960  sineq0  21963  explog  22022  reexplog  22023  eflogeq  22030  abslogle  22047  tanarg  22048  logtayl  22085  logtayl2  22087  ang180lem3  22187  affineequiv  22201  affineequiv2  22202  chordthmlem4  22210  chordthmlem5  22211  heron  22213  dcubic1lem  22218  dcubic2  22219  dcubic  22221  mcubic  22222  cubic2  22223  dquartlem1  22226  dquart  22228  quart1lem  22230  quartlem1  22232  quart  22236  acoscos  22268  atanlogaddlem  22288  atantayl2  22313  atantayl3  22314  birthdaylem2  22326  efrlim  22343  amgmlem  22363  logdifbnd  22367  emcllem3  22371  emcllem6  22374  basellem3  22400  basellem8  22405  basellem9  22406  chtprm  22471  logfaclbnd  22541  perfect1  22547  bcp1ctr  22598  bclbnd  22599  bposlem1  22603  lgsdilem  22641  lgsdirnn0  22658  lgsdinn0  22659  lgseisenlem2  22669  lgsquadlem1  22673  2sqlem2  22683  mul2sq  22684  vmadivsum  22711  rpvmasumlem  22716  dchrisumlem1  22718  dchrisumlem2  22719  dchrmusum2  22723  dchrvmasum2if  22726  dchrisum0lem2  22747  logsqvma2  22772  selberg3  22788  selberg4lem1  22789  pntrsumo1  22794  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem5  22810  pntibndlem2  22820  pntlemk  22835  pntlemo  22836  ostth2lem4  22865  ostth3  22867  tgcgrextend  22919  tgbtwndiff  22939  tgifscgr  22941  trgcgrg  22947  tgidinside  22983  tgbtwnconn1lem1  22984  tgbtwnconn1lem2  22985  tgbtwnconn1lem3  22986  ismir  23043  miriso  23051  krippenlem  23061  midexlem  23063  ragmir  23071  brbtwn2  23119  colinearalglem4  23123  axsegconlem1  23131  axpaschlem  23154  axcontlem4  23181  axcontlem7  23184  axcontlem8  23185  grpoidinvlem2  23660  gxid  23728  subgores  23759  nvmtri  24027  cnnvm  24041  nvnd  24047  ipidsq  24076  ipnm  24077  ipipcj  24081  blocnilem  24172  ipasslem2  24200  dipsubdir  24216  hvaddsubval  24403  pjhthlem1  24762  pjspansn  24948  pjo  25042  unoplin  25292  adjadj  25308  hmoplin  25314  eigvec1  25334  lnopeqi  25380  nmcexi  25398  lnfnsubi  25418  riesz3i  25434  kbass6  25493  leoprf2  25499  leoprf  25500  pjnmopi  25520  mdslmd1lem1  25697  mdslmd1lem2  25698  superpos  25726  fgreu  25958  resf1o  25998  xrge0tsmseq  26223  subrgchr  26230  rhmdvd  26257  pstmval  26291  mndpluscn  26325  qqhucn  26390  esumval  26469  gsumesum  26479  esumcst  26483  esumpcvgval  26496  oddpwdc  26706  eulerpartlemgvv  26728  sseqp1  26747  probdif  26772  ballotlemfp1  26843  sgnmul  26894  signsvtn  26954  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamgulmlem4  26987  lgamgulmlem5  26988  gamigam  27008  lgamcvg2  27010  gamfac  27022  derangen2  27031  subfaclefac  27033  subfaclim  27045  sinccvglem  27286  fprodshft  27456  fprodrev  27457  iprodclim3  27469  binomfallfaclem2  27512  ltflcei  28390  mblfinlem4  28402  ibladdnclem  28419  iblabsnc  28427  iblmulc2nc  28428  ftc1anclem6  28443  ftc1anclem8  28445  filnetlem4  28573  sdclem2  28609  ismtycnv  28672  heiborlem10  28690  mzpsubmpt  29050  irrapxlem3  29136  pellexlem6  29146  pell1234qrne0  29165  pell1234qrreccl  29166  pell1234qrmulcl  29167  pell14qrdich  29181  pell1qrgaplem  29185  rmxluc  29248  rmyluc  29249  jm2.24nn  29273  jm2.18  29308  jm2.19lem2  29310  jm2.19lem3  29311  jm2.22  29315  jm2.23  29316  jm2.16nn0  29324  jm2.27c  29327  fnwe2lem2  29375  lmhmfgsplit  29410  hbtlem2  29451  hashgcdeq  29537  dvconstbi  29579  stoweidlem22  29788  stoweidlem32  29798  wallispilem5  29835  stirlinglem5  29844  sigarcol  29871  elovmpt3rab1  30134  mulsubfacd  30143  powm2modprm  30219  wwlkextwrd  30331  clwwlkn2  30409  clwlkisclwwlklem2a3  30414  clwlkisclwwlk2  30423  clwwlkel  30426  clwwlkfo  30430  clwwlkext2edg  30435  wwlkext2clwwlk  30436  cshwlemma1  30460  frg2woteq  30624  extwwlkfablem1  30638  clwwlkextfrlem1  30640  numclwlk1lem2foa  30655  numclwlk1lem2fo  30659  numclwlk2lem2f  30667  lincext3  30921  lincresunit3  30946  recsec  31022  reccsc  31023  bnj1415  31958  lflvsass  32619  lkrscss  32636  eqlkr  32637  eqlkr3  32639  ldualvsdi2  32682  omllaw3  32783  cmtcomlemN  32786  cmtbr3N  32792  omlfh3N  32797  llnexchb2lem  33405  dalawlem7  33414  dalawlem11  33418  dalawlem12  33419  pol1N  33447  paddatclN  33486  4atexlemcnd  33609  ltrncoidN  33665  cdleme3b  33766  cdleme11  33807  cdleme15a  33811  cdleme22e  33881  cdleme22g  33885  cdlemg18b  34216  trlcoat  34260  cdlemk2  34369  cdlemk4  34371  cdlemki  34378  cdlemksv2  34384  cdlemk15  34392  cdlemk55a  34496  diainN  34595  dia2dimlem3  34604  dia2dimlem5  34606  dvhlveclem  34646  diaocN  34663  cdlemn4  34736  cdlemn8  34742  dihopelvalcpre  34786  dihmeetlem9N  34853  dih1dimatlem  34867  dihpN  34874  dochvalr3  34901  dochsat  34921  djhjlj  34941  dochdmm1  34948  dihjatcclem4  34959  dihjat1  34967  dihjat4  34971  dochsnkr2cl  35012  dochfl1  35014  lclkrlem2j  35054  mapdordlem2  35175  mapdrvallem2  35183  hdmap10  35381