Theorem eqtr2d 2424

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

Syntax hints:   -> wi 4   = wceq 1399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360

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

This theorem is referenced by:  3eqtrrd  2428  3eqtr2rd  2430  ifan  3903  ifor  3904  dfopif  4128  nvocnv  6088  elovmpt3rab1  6435  onsucmin  6555  csbopeq1a  6752  oaabs2  7212  ecinxp  7304  resixpfo  7426  sbthlem3  7548  rankxpsuc  8213  fseqenlem2  8319  dfac2  8424  isf32lem9  8654  compsscnvlem  8663  ttukeylem7  8808  fpwwe2lem11  8929  00id  9666  submul2  9915  mulsubfacd  9934  divadddiv  10176  infmsup  10437  xadd4d  11416  fzdifsuc  11661  fzval3  11784  fzoshftral  11822  ceim1l  11874  fldiv  11887  flmod  11911  intfrac  11912  modcyc2  11933  moddi  11957  uzrdgfni  11972  axdc4uzlem  11995  seqf1olem1  12049  seqf1olem2  12050  seqid2  12056  expnegz  12103  binom2sub  12187  binom3  12189  wrdlenccats1lenm1  12536  ccatw2s1p2  12550  ccats1swrdeq  12605  swrdccatin12lem2  12625  swrdccatin12  12627  swrdccat3b  12632  cshweqrep  12700  2cshwcshw  12704  ccatco  12712  swrds2  12794  relexpsucnnr  12862  relexpaddnn  12886  reim  12944  mulre  12956  addcj  12983  absimle  13144  clim2ser  13479  isercoll2  13493  serf0  13505  iseralt  13509  summolem3  13538  isumclim3  13576  mptfzshft  13595  fsumrev  13596  fsum2mul  13606  incexc  13651  isumsplit  13654  mertenslem1  13695  fprodrev  13783  iprodclim3  13795  ef4p  13850  tanval3  13871  efival  13889  sinmul  13909  bitsinvp1  14101  sadaddlem  14118  bitsshft  14127  smu01lem  14137  eulerthlem2  14314  powm2modprm  14330  pythagtriplem16  14356  pczpre  14373  pcqdiv  14383  pcadd  14410  pcfac  14420  prmreclem5  14440  4sqlem10  14467  4sqlem19  14483  vdwapun  14494  vdwlem1  14501  ramcl  14549  strfvd  14667  strfv2d  14668  xpsff1o  14975  xpslem  14980  2oppccomf  15131  oppcepi  15145  sscfn1  15223  sscfn2  15224  invfuc  15380  funcestrcsetclem7  15532  funcsetcestrclem7  15547  grpinvssd  16232  grpinvval2  16238  pmtrdifwrdellem2  16624  psgnunilem1  16635  psgnuni  16641  pgp0  16733  sylow1lem1  16735  sylow3lem2  16765  efgredleme  16878  efgcpbllemb  16890  frgpuptinv  16906  frgpup3lem  16912  gexexlem  16975  cyggenod  17004  gsumval3eu  17024  gsumval3OLD  17025  gsumval3  17028  gsumzaddlem  17051  gsumzaddlemOLD  17053  dprd2db  17205  ringinvdv  17456  lss1d  17722  pwssplit1  17818  mplcoe3  18241  mplcoe3OLD  18242  subrgascl  18276  evlseu  18298  ply1sclid  18442  znzrh2  18675  regsumsupp  18749  ipassr2  18773  dsmmfi  18860  frlmlss  18873  frlmip  18898  frlmlbs  18917  frlmup3  18920  islindf4  18958  1marepvmarrepid  19162  madurid  19231  smadiadetlem3  19255  mat2pmatghm  19316  pmatcollpwscmatlem1  19375  pm2mpmhmlem2  19405  cpmadurid  19453  cpmidgsumm2pm  19455  cpmadugsumlemB  19460  cayhamlem2  19470  ntrval2  19637  ordtuni  19777  cnclima  19855  cmpsub  19986  ptbasfi  20167  txbasval  20192  pt1hmeo  20392  alexsubALTlem1  20632  trust  20817  ussid  20848  ressuss  20851  ressprdsds  20959  imasdsf1olem  20961  setsms  21068  tmsxms  21074  tmsxpsmopn  21125  subgnm  21232  tngnm  21250  tngngp2  21251  xrsxmet  21399  xrge0gsumle  21423  metdstri  21440  xrhmeo  21531  lebnumlem3  21548  pcorevlem  21611  pi1xfrcnvlem  21641  clmabs  21667  cvsmuleqdivd  21696  rrxip  21907  rrxds  21910  minveclem4a  21930  pjthlem1  21937  ovolunlem1a  21992  mbfres2  22137  i1faddlem  22185  ibladdlem  22311  iblabs  22320  ditgsplit  22350  dvnres  22419  dveflem  22465  dveq0  22486  dvfsumabs  22509  itgsubstlem  22534  ply1divex  22622  dgrco  22757  plycjlem  22758  taylthlem1  22853  pserdv2  22910  abelthlem6  22916  abelthlem7  22918  tangtx  22983  abssinper  22996  sineq0  22999  explog  23066  reexplog  23067  eflogeq  23074  abslogle  23090  tanarg  23091  logtayl  23128  logtayl2  23130  relogbdiv  23237  ang180lem3  23261  affineequiv  23273  affineequiv2  23274  chordthmlem4  23282  chordthmlem5  23283  heron  23285  dcubic1lem  23290  dcubic2  23291  dcubic  23293  mcubic  23294  cubic2  23295  dquartlem1  23298  dquart  23300  quart1lem  23302  quartlem1  23304  quart  23308  acoscos  23340  atanlogaddlem  23360  atantayl2  23385  atantayl3  23386  birthdaylem2  23399  efrlim  23416  amgmlem  23436  logdifbnd  23440  emcllem3  23444  emcllem6  23447  basellem3  23473  basellem8  23478  basellem9  23479  chtprm  23544  logfaclbnd  23614  perfect1  23620  bcp1ctr  23671  bclbnd  23672  bposlem1  23676  lgsdilem  23714  lgsdirnn0  23731  lgsdinn0  23732  lgseisenlem2  23742  lgsquadlem1  23746  2sqlem2  23756  mul2sq  23757  vmadivsum  23784  rpvmasumlem  23789  dchrisumlem1  23791  dchrisumlem2  23792  dchrmusum2  23796  dchrvmasum2if  23799  dchrisum0lem2  23820  logsqvma2  23845  selberg3  23861  selberg4lem1  23862  pntrsumo1  23867  pntrlog2bndlem2  23880  pntrlog2bndlem3  23881  pntrlog2bndlem5  23883  pntibndlem2  23893  pntlemk  23908  pntlemo  23909  ostth2lem4  23938  ostth3  23940  tgbtwndiff  24017  tgifscgr  24020  trgcgrg  24026  motcgr3  24052  tgbtwnconn1lem1  24079  tgbtwnconn1lem2  24080  ismir  24160  miriso  24170  midexlem  24189  ragmir  24197  footex  24215  colperpexlem3  24226  mideulem2  24228  midex  24231  opphllem3  24241  midcgr  24266  lmiisolem  24281  brbtwn2  24329  colinearalglem4  24333  axsegconlem1  24341  axpaschlem  24364  axcontlem4  24391  axcontlem7  24394  axcontlem8  24395  wwlkextwrd  24849  clwwlkn2  24896  clwlkisclwwlklem2a3  24902  clwlkisclwwlk2  24911  clwwlkel  24914  clwwlkfo  24918  clwwlkext2edg  24923  wwlkext2clwwlk  24924  frg2woteq  25181  extwwlkfablem1  25195  clwwlkextfrlem1  25197  numclwlk1lem2foa  25212  numclwlk1lem2fo  25216  numclwlk2lem2f  25224  grpoidinvlem2  25324  gxid  25392  subgores  25423  nvmtri  25691  cnnvm  25705  nvnd  25711  ipidsq  25740  ipnm  25741  ipipcj  25745  blocnilem  25836  ipasslem2  25864  dipsubdir  25880  hvaddsubval  26067  pjhthlem1  26426  pjspansn  26612  pjo  26706  unoplin  26955  adjadj  26971  hmoplin  26977  eigvec1  26997  lnopeqi  27043  nmcexi  27061  lnfnsubi  27081  riesz3i  27097  kbass6  27156  leoprf2  27162  leoprf  27163  pjnmopi  27183  mdslmd1lem1  27360  mdslmd1lem2  27361  superpos  27389  fgreu  27659  resf1o  27703  2sqmod  27789  gsummpt2d  27925  xrge0tsmseq  27931  subrgchr  27938  rhmdvd  27965  qtophaus  27993  pstmval  28028  mndpluscn  28062  qqhucn  28126  esumval  28194  gsumesum  28207  esumcst  28211  esumpcvgval  28226  oddpwdc  28476  eulerpartlemgvv  28498  probdif  28542  ballotlemfp1  28613  sgnmul  28664  signsvtn  28724  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem4  28763  lgamgulmlem5  28764  gamigam  28784  lgamcvg2  28786  gamfac  28798  derangen2  28807  subfaclefac  28809  subfaclim  28821  mrsubrn  29062  sinccvglem  29227  binomfallfaclem2  29328  ltflcei  30208  mblfinlem4  30219  ibladdnclem  30237  iblabsnc  30245  iblmulc2nc  30246  ftc1anclem6  30261  ftc1anclem8  30263  filnetlem4  30365  sdclem2  30401  ismtycnv  30464  heiborlem10  30482  mzpsubmpt  30841  irrapxlem3  30925  pellexlem6  30935  pell1234qrne0  30954  pell1234qrreccl  30955  pell1234qrmulcl  30956  pell14qrdich  30970  pell1qrgaplem  30974  rmxluc  31037  rmyluc  31038  jm2.24nn  31062  jm2.18  31096  jm2.19lem2  31098  jm2.19lem3  31099  jm2.22  31103  jm2.23  31104  jm2.16nn0  31112  jm2.27c  31115  fnwe2lem2  31163  lmhmfgsplit  31198  hbtlem2  31241  hashgcdeq  31326  lcmgcdlem  31380  dvconstbi  31407  bccm1k  31415  binomcxplemnotnn0  31429  fmptsnxp  31611  lefldiveq  31649  lt4addmuld  31672  fzdifsuc2  31678  fsumnncl  31738  limcperiod  31800  sumnnodd  31802  limcresiooub  31814  limcresioolb  31815  0ellimcdiv  31821  reclimc  31825  sinmulcos  31831  coskpi2  31832  divcncf  31852  cncfdmsn  31859  cncfiooicclem1  31862  dvmptdiv  31880  fperdvper  31881  dvmptresicc  31882  dvnmptdivc  31901  dvnxpaek  31905  dvnmul  31906  dvnprodlem1  31909  dvnprodlem3  31911  itgcoscmulx  31934  itgsincmulx  31939  itgspltprt  31944  itgiccshift  31945  itgperiod  31946  stoweidlem22  31970  stoweidlem32  31980  wallispilem5  32017  stirlinglem5  32026  dirkertrigeqlem2  32047  dirkertrigeq  32049  dirkercncflem1  32051  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem13  32068  fourierdlem16  32071  fourierdlem19  32074  fourierdlem21  32076  fourierdlem22  32077  fourierdlem28  32083  fourierdlem32  32087  fourierdlem33  32088  fourierdlem42  32097  fourierdlem47  32102  fourierdlem48  32103  fourierdlem49  32104  fourierdlem50  32105  fourierdlem56  32111  fourierdlem60  32115  fourierdlem61  32116  fourierdlem64  32119  fourierdlem66  32121  fourierdlem71  32126  fourierdlem73  32128  fourierdlem74  32129  fourierdlem76  32131  fourierdlem78  32133  fourierdlem79  32134  fourierdlem80  32135  fourierdlem81  32136  fourierdlem83  32138  fourierdlem88  32143  fourierdlem92  32147  fourierdlem93  32148  fourierdlem97  32152  fourierdlem101  32156  fourierdlem103  32158  fourierdlem104  32159  fourierdlem109  32164  fourierdlem111  32166  fouriersw  32180  elaa2lem  32182  etransclem24  32207  etransclem25  32208  etransclem35  32218  etransclem46  32229  sigarcol  32247  nn0onn0exALTV  32540  ccats1pfxeq  32596  pfxccatin12lem2  32599  pfxccatin12  32600  c0snmgmhm  32920  rngcifuestrc  33005  funcrngcsetc  33006  funcrngcsetcALT  33007  funcringcsetc  33043  funcringcsetcALTV2lem7  33050  funcringcsetclem7ALTV  33073  lincext3  33257  lincresunit3  33282  nn0onn0ex  33341  nnpw2pmod  33404  blennn0em1  33412  digexp  33428  dignn0ehalf  33438  nn0mulfsum  33445  recsec  33486  reccsc  33487  aacllem  33550  bnj1415  34441  lflvsass  35219  lkrscss  35236  eqlkr  35237  eqlkr3  35239  ldualvsdi2  35282  omllaw3  35383  cmtcomlemN  35386  cmtbr3N  35392  omlfh3N  35397  llnexchb2lem  36005  dalawlem7  36014  dalawlem11  36018  dalawlem12  36019  pol1N  36047  paddatclN  36086  4atexlemcnd  36209  ltrncoidN  36265  cdleme3b  36367  cdleme11  36408  cdleme15a  36412  cdleme22e  36483  cdleme22g  36487  cdlemg18b  36818  trlcoat  36862  cdlemk2  36971  cdlemk4  36973  cdlemki  36980  cdlemksv2  36986  cdlemk15  36994  cdlemk55a  37098  diainN  37197  dia2dimlem3  37206  dia2dimlem5  37208  dvhlveclem  37248  diaocN  37265  cdlemn4  37338  cdlemn8  37344  dihopelvalcpre  37388  dihmeetlem9N  37455  dih1dimatlem  37469  dihpN  37476  dochvalr3  37503  dochsat  37523  djhjlj  37543  dochdmm1  37550  dihjatcclem4  37561  dihjat1  37569  dihjat4  37573  dochsnkr2cl  37614  dochfl1  37616  lclkrlem2j  37656  mapdordlem2  37777  mapdrvallem2  37785  hdmap10  37983  relexpmulnn  38245  relexpmulg  38246  int-addassocd  38524