Theorem eqtr2d 2509

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

Syntax hints:   -> wi 4   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

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

This theorem is referenced by:  3eqtrrd  2513  3eqtr2rd  2515  ifan  3985  ifor  3986  dfopif  4210  nvocnv  6173  elovmpt3rab1  6518  onsucmin  6634  csbopeq1a  6834  oaabs2  7291  ecinxp  7383  resixpfo  7504  sbthlem3  7626  rankxpsuc  8296  fseqenlem2  8402  dfac2  8507  isf32lem9  8737  compsscnvlem  8746  ttukeylem7  8891  fpwwe2lem11  9014  00id  9750  submul2  9993  mulsubfacd  10012  divadddiv  10255  infmsup  10517  xadd4d  11491  fzdifsuc  11735  fzval3  11849  fzoshftral  11887  ceim1l  11938  fldiv  11951  flmod  11974  intfrac  11975  modcyc2  11996  moddi  12018  uzrdgfni  12033  axdc4uzlem  12056  seqf1olem1  12110  seqf1olem2  12111  seqid2  12117  expnegz  12164  binom2sub  12249  binom3  12251  ccats1swrdeq  12653  swrdccatin12lem2  12673  swrdccatin12  12675  swrdccat3b  12680  cshweqrep  12748  2cshwcshw  12752  ccatco  12760  swrds2  12842  reim  12901  mulre  12913  addcj  12940  absimle  13101  clim2ser  13436  isercoll2  13450  serf0  13462  iseralt  13466  summolem3  13495  isumclim3  13533  mptfzshft  13552  fsumrev  13553  fsum2mul  13563  incexc  13608  isumsplit  13611  mertenslem1  13652  ef4p  13705  tanval3  13726  efival  13744  sinmul  13764  bitsinvp1  13954  sadaddlem  13971  bitsshft  13980  smu01lem  13990  eulerthlem2  14167  powm2modprm  14183  pythagtriplem16  14209  pczpre  14226  pcqdiv  14236  pcadd  14263  pcfac  14273  prmreclem5  14293  4sqlem10  14320  4sqlem19  14336  vdwapun  14347  vdwlem1  14354  ramcl  14402  strfvd  14517  strfv2d  14518  xpsff1o  14819  xpslem  14824  2oppccomf  14977  oppcepi  14991  sscfn1  15043  sscfn2  15044  invfuc  15197  grpinvssd  15916  grpinvval2  15922  pmtrdifwrdellem2  16303  psgnunilem1  16314  psgnuni  16320  pgp0  16412  sylow1lem1  16414  sylow3lem2  16444  efgredleme  16557  efgcpbllemb  16569  frgpuptinv  16585  frgpup3lem  16591  gexexlem  16651  cyggenod  16678  gsumval3eu  16698  gsumval3OLD  16699  gsumval3  16702  gsumzaddlem  16725  gsumzaddlemOLD  16727  dprd2db  16882  rnginvdv  17127  lss1d  17392  pwssplit1  17488  mplcoe3  17899  mplcoe3OLD  17900  subrgascl  17934  evlseu  17956  ply1sclid  18100  znzrh2  18351  regsumsupp  18425  ipassr2  18449  dsmmfi  18536  frlmlss  18549  frlmip  18576  frlmlbs  18598  frlmup3  18601  islindf4  18640  1marepvmarrepid  18844  madurid  18913  smadiadetlem3  18937  mat2pmatghm  18998  pmatcollpwscmatlem1  19057  pm2mpmhmlem2  19087  cpmadurid  19135  cpmidgsumm2pm  19137  cayhamlem2  19152  ntrval2  19318  ordtuni  19457  cnclima  19535  cmpsub  19666  ptbasfi  19817  txbasval  19842  pt1hmeo  20042  alexsubALTlem1  20282  trust  20467  ussid  20498  ressuss  20501  ressprdsds  20609  imasdsf1olem  20611  setsms  20718  tmsxms  20724  tmsxpsmopn  20775  subgnm  20882  tngnm  20900  tngngp2  20901  xrsxmet  21049  xrge0gsumle  21073  metdstri  21090  xrhmeo  21181  lebnumlem3  21198  pcorevlem  21261  pi1xfrcnvlem  21291  clmabs  21317  cvsmuleqdivd  21346  rrxip  21557  rrxds  21560  minveclem4a  21580  pjthlem1  21587  ovolunlem1a  21642  mbfres2  21787  i1faddlem  21835  ibladdlem  21961  iblabs  21970  ditgsplit  22000  dvnres  22069  dveflem  22115  dveq0  22136  dvfsumabs  22159  itgsubstlem  22184  ply1divex  22272  dgrco  22406  plycjlem  22407  taylthlem1  22502  pserdv2  22559  abelthlem6  22565  abelthlem7  22567  tangtx  22631  abssinper  22644  sineq0  22647  explog  22706  reexplog  22707  eflogeq  22714  abslogle  22731  tanarg  22732  logtayl  22769  logtayl2  22771  ang180lem3  22871  affineequiv  22885  affineequiv2  22886  chordthmlem4  22894  chordthmlem5  22895  heron  22897  dcubic1lem  22902  dcubic2  22903  dcubic  22905  mcubic  22906  cubic2  22907  dquartlem1  22910  dquart  22912  quart1lem  22914  quartlem1  22916  quart  22920  acoscos  22952  atanlogaddlem  22972  atantayl2  22997  atantayl3  22998  birthdaylem2  23010  efrlim  23027  amgmlem  23047  logdifbnd  23051  emcllem3  23055  emcllem6  23058  basellem3  23084  basellem8  23089  basellem9  23090  chtprm  23155  logfaclbnd  23225  perfect1  23231  bcp1ctr  23282  bclbnd  23283  bposlem1  23287  lgsdilem  23325  lgsdirnn0  23342  lgsdinn0  23343  lgseisenlem2  23353  lgsquadlem1  23357  2sqlem2  23367  mul2sq  23368  vmadivsum  23395  rpvmasumlem  23400  dchrisumlem1  23402  dchrisumlem2  23403  dchrmusum2  23407  dchrvmasum2if  23410  dchrisum0lem2  23431  logsqvma2  23456  selberg3  23472  selberg4lem1  23473  pntrsumo1  23478  pntrlog2bndlem2  23491  pntrlog2bndlem3  23492  pntrlog2bndlem5  23494  pntibndlem2  23504  pntlemk  23519  pntlemo  23520  ostth2lem4  23549  ostth3  23551  tgcgrextend  23604  tgbtwndiff  23625  tgifscgr  23628  trgcgrg  23634  motcgr3  23660  tgidinside  23685  tgbtwnconn1lem1  23686  tgbtwnconn1lem2  23687  tgbtwnconn1lem3  23688  ismir  23753  miriso  23763  krippenlem  23775  midexlem  23777  ragmir  23785  footex  23803  colperpexlem3  23811  mideulem  23813  mideu  23814  midcgr  23823  lmiisolem  23838  brbtwn2  23884  colinearalglem4  23888  axsegconlem1  23896  axpaschlem  23919  axcontlem4  23946  axcontlem7  23949  axcontlem8  23950  wwlkextwrd  24404  clwwlkn2  24451  clwlkisclwwlklem2a3  24457  clwlkisclwwlk2  24466  clwwlkel  24469  clwwlkfo  24473  clwwlkext2edg  24478  wwlkext2clwwlk  24479  frg2woteq  24737  extwwlkfablem1  24751  clwwlkextfrlem1  24753  numclwlk1lem2foa  24768  numclwlk1lem2fo  24772  numclwlk2lem2f  24780  grpoidinvlem2  24883  gxid  24951  subgores  24982  nvmtri  25250  cnnvm  25264  nvnd  25270  ipidsq  25299  ipnm  25300  ipipcj  25304  blocnilem  25395  ipasslem2  25423  dipsubdir  25439  hvaddsubval  25626  pjhthlem1  25985  pjspansn  26171  pjo  26265  unoplin  26515  adjadj  26531  hmoplin  26537  eigvec1  26557  lnopeqi  26603  nmcexi  26621  lnfnsubi  26641  riesz3i  26657  kbass6  26716  leoprf2  26722  leoprf  26723  pjnmopi  26743  mdslmd1lem1  26920  mdslmd1lem2  26921  superpos  26949  fgreu  27185  resf1o  27225  xrge0tsmseq  27440  subrgchr  27447  rhmdvd  27474  pstmval  27510  mndpluscn  27544  qqhucn  27609  qtophaus  27637  esumval  27697  gsumesum  27707  esumcst  27711  esumpcvgval  27724  oddpwdc  27933  eulerpartlemgvv  27955  sseqp1  27974  probdif  27999  ballotlemfp1  28070  sgnmul  28121  signsvtn  28181  lgamgulmlem2  28212  lgamgulmlem3  28213  lgamgulmlem4  28214  lgamgulmlem5  28215  gamigam  28235  lgamcvg2  28237  gamfac  28249  derangen2  28258  subfaclefac  28260  subfaclim  28272  sinccvglem  28513  fprodshft  28683  fprodrev  28684  iprodclim3  28696  binomfallfaclem2  28739  ltflcei  29620  mblfinlem4  29631  ibladdnclem  29648  iblabsnc  29656  iblmulc2nc  29657  ftc1anclem6  29672  ftc1anclem8  29674  filnetlem4  29802  sdclem2  29838  ismtycnv  29901  heiborlem10  29919  mzpsubmpt  30279  irrapxlem3  30364  pellexlem6  30374  pell1234qrne0  30393  pell1234qrreccl  30394  pell1234qrmulcl  30395  pell14qrdich  30409  pell1qrgaplem  30413  rmxluc  30476  rmyluc  30477  jm2.24nn  30501  jm2.18  30534  jm2.19lem2  30536  jm2.19lem3  30537  jm2.22  30541  jm2.23  30542  jm2.16nn0  30550  jm2.27c  30553  fnwe2lem2  30601  lmhmfgsplit  30636  hbtlem2  30677  hashgcdeq  30763  lcmgcdlem  30812  dvconstbi  30839  fmptsnxp  31022  dstregt0  31040  lefldiveq  31059  lt4addmuld  31083  ssfiunibd  31086  tgiooss  31110  divcnvg  31169  limcperiod  31170  sumnnodd  31172  islpcn  31181  0ellimcdiv  31191  reclimc  31195  sinmulcos  31201  coskpi2  31202  cncfperiod  31217  divcncf  31222  cncfuni  31225  cncfiooicclem1  31232  dvsinax  31241  dvmptdiv  31247  fperdvper  31248  ioodvbdlimc2lem  31264  itgioocnicc  31295  itgiccshift  31298  itgperiod  31299  stoweidlem22  31322  stoweidlem32  31332  wallispilem5  31369  stirlinglem5  31378  dirkertrigeqlem2  31399  dirkertrigeq  31401  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem6  31413  fourierdlem16  31423  fourierdlem19  31426  fourierdlem21  31428  fourierdlem22  31429  fourierdlem26  31433  fourierdlem28  31435  fourierdlem32  31439  fourierdlem33  31440  fourierdlem38  31445  fourierdlem41  31448  fourierdlem42  31449  fourierdlem47  31454  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem56  31463  fourierdlem60  31467  fourierdlem61  31468  fourierdlem62  31469  fourierdlem64  31471  fourierdlem65  31472  fourierdlem71  31478  fourierdlem73  31480  fourierdlem74  31481  fourierdlem76  31483  fourierdlem78  31485  fourierdlem79  31486  fourierdlem80  31487  fourierdlem81  31488  fourierdlem83  31490  fourierdlem84  31491  fourierdlem88  31495  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem92  31499  fourierdlem93  31500  fourierdlem97  31504  fourierdlem98  31505  fourierdlem101  31508  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem109  31516  fourierdlem111  31518  fourierdlem113  31520  fourierdlem114  31521  fourierswlem  31531  fouriersw  31532  sigarcol  31548  lincext3  32130  lincresunit3  32155  recsec  32231  reccsc  32232  bnj1415  33173  lflvsass  33878  lkrscss  33895  eqlkr  33896  eqlkr3  33898  ldualvsdi2  33941  omllaw3  34042  cmtcomlemN  34045  cmtbr3N  34051  omlfh3N  34056  llnexchb2lem  34664  dalawlem7  34673  dalawlem11  34677  dalawlem12  34678  pol1N  34706  paddatclN  34745  4atexlemcnd  34868  ltrncoidN  34924  cdleme3b  35025  cdleme11  35066  cdleme15a  35070  cdleme22e  35140  cdleme22g  35144  cdlemg18b  35475  trlcoat  35519  cdlemk2  35628  cdlemk4  35630  cdlemki  35637  cdlemksv2  35643  cdlemk15  35651  cdlemk55a  35755  diainN  35854  dia2dimlem3  35863  dia2dimlem5  35865  dvhlveclem  35905  diaocN  35922  cdlemn4  35995  cdlemn8  36001  dihopelvalcpre  36045  dihmeetlem9N  36112  dih1dimatlem  36126  dihpN  36133  dochvalr3  36160  dochsat  36180  djhjlj  36200  dochdmm1  36207  dihjatcclem4  36218  dihjat1  36226  dihjat4  36230  dochsnkr2cl  36271  dochfl1  36273  lclkrlem2j  36313  mapdordlem2  36434  mapdrvallem2  36442  hdmap10  36640