Theorem eqtr2d 2458

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

Syntax hints:   -> wi 4   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-cleq 2416

This theorem is referenced by:  3eqtrrd  2462  3eqtr2rd  2464  ifan  3895  ifor  3896  dfopif  4122  nvocnv  6134  elovmpt3rab1  6480  onsucmin  6601  csbopeq1a  6799  oaabs2  7296  ecinxp  7388  resixpfo  7510  sbthlem3  7632  rankxpsuc  8300  fseqenlem2  8402  dfac2  8507  isf32lem9  8737  compsscnvlem  8746  ttukeylem7  8891  fpwwe2lem11  9011  00id  9754  submul2  10005  mulsubfacd  10024  divadddiv  10268  infrenegsup  10537  infmsupOLD  10538  xadd4d  11535  fzdifsuc  11801  fzval3  11928  fzoshftral  11967  ceim1l  12019  fldiv  12032  flmod  12056  intfrac  12057  modcyc2  12078  moddi  12102  uzrdgfni  12117  axdc4uzlem  12140  seqf1olem1  12197  seqf1olem2  12198  seqid2  12204  expnegz  12251  binom2sub  12336  binom3  12338  wrdlenccats1lenm1  12697  ccatw2s1p2  12711  ccats1swrdeq  12766  swrdccatin12lem2  12786  swrdccatin12  12788  swrdccat3b  12793  cshweqrep  12861  2cshwcshw  12865  ccatco  12873  swrds2  12959  relexpsucnnr  13027  relexpaddnn  13053  reim  13111  mulre  13123  addcj  13150  absimle  13311  clim2ser  13656  isercoll2  13670  serf0  13685  iseralt  13689  summolem3  13718  isumclim3  13758  mptfzshft  13777  fsumrev  13778  fsum2mul  13788  incexc  13833  isumsplit  13836  mertenslem1  13878  fprodrev  13969  iprodclim3  13991  binomfallfaclem2  14031  ef4p  14105  tanval3  14126  efival  14144  sinmul  14164  bitsinvp1  14361  sadaddlem  14378  bitsshft  14387  smu01lem  14397  lcmgcdlem  14509  lcm1  14513  lcmfass  14557  eulerthlem2  14668  powm2modprm  14692  pythagtriplem16  14718  pczpre  14735  pcqdiv  14745  pcadd  14772  pcfac  14782  prmreclem5  14802  4sqlem10  14829  4sqlem19  14851  vdwapun  14862  vdwlem1  14869  ramcl  14925  strfvd  15092  strfv2d  15093  xpsff1o  15412  xpslem  15417  2oppccomf  15568  oppcepi  15582  sscfn1  15660  sscfn2  15661  invfuc  15817  funcestrcsetclem7  15969  funcsetcestrclem7  15984  grpinvssd  16669  grpinvval2  16675  pmtrdifwrdellem2  17061  psgnunilem1  17072  psgnuni  17078  pgp0  17186  sylow1lem1  17188  sylow3lem2  17218  efgredleme  17331  efgcpbllemb  17343  frgpuptinv  17359  frgpup3lem  17365  gexexlem  17428  cyggenod  17457  gsumval3eu  17476  gsumval3  17479  gsumzaddlem  17492  dprd2db  17614  ringinvdv  17860  lss1d  18124  pwssplit1  18220  mplcoe3  18628  subrgascl  18659  evlseu  18677  ply1sclid  18819  znzrh2  19053  regsumsupp  19127  ipassr2  19151  dsmmfi  19238  frlmlss  19251  frlmip  19273  frlmlbs  19292  frlmup3  19295  islindf4  19333  1marepvmarrepid  19537  madurid  19606  smadiadetlem3  19630  mat2pmatghm  19691  pmatcollpwscmatlem1  19750  pm2mpmhmlem2  19780  cpmadurid  19828  cpmidgsumm2pm  19830  cpmadugsumlemB  19835  cayhamlem2  19845  ntrval2  20003  ordtuni  20143  cnclima  20221  cmpsub  20352  ptbasfi  20533  txbasval  20558  pt1hmeo  20758  alexsubALTlem1  20999  trust  21181  ussid  21212  ressuss  21215  ressprdsds  21323  imasdsf1olem  21325  setsms  21432  tmsxms  21438  tmsxpsmopn  21489  subgnm  21578  tngnm  21596  tngngp2  21597  xrsxmet  21764  xrge0gsumle  21788  metdstri  21805  metdstriOLD  21820  xrhmeo  21911  lebnumlem3  21928  lebnumlem3OLD  21931  pcorevlem  21994  pi1xfrcnvlem  22024  clmabs  22050  cvsmuleqdivd  22079  rrxip  22286  rrxds  22289  minveclem4a  22309  minveclem4aOLD  22321  pjthlem1  22328  ovolunlem1a  22386  mbfres2  22538  i1faddlem  22588  ibladdlem  22714  iblabs  22723  ditgsplit  22753  dvnres  22822  dveflem  22868  dveq0  22889  dvfsumabs  22912  itgsubstlem  22937  ply1divex  23024  dgrco  23166  plycjlem  23167  taylthlem1  23265  pserdv2  23322  abelthlem6  23328  abelthlem7  23330  tangtx  23397  abssinper  23410  sineq0  23413  explog  23480  reexplog  23481  eflogeq  23488  abslogle  23504  tanarg  23505  logtayl  23542  logtayl2  23544  relogbdiv  23653  ang180lem3  23677  affineequiv  23689  affineequiv2  23690  chordthmlem4  23698  chordthmlem5  23699  heron  23701  dcubic1lem  23706  dcubic2  23707  dcubic  23709  mcubic  23710  cubic2  23711  dquartlem1  23714  dquart  23716  quart1lem  23718  quartlem1  23720  quart  23724  acoscos  23756  atanlogaddlem  23776  atantayl2  23801  atantayl3  23802  birthdaylem2  23815  efrlim  23832  amgmlem  23852  logdifbnd  23856  emcllem3  23860  emcllem6  23863  lgamgulmlem2  23892  lgamgulmlem3  23893  lgamgulmlem4  23894  lgamgulmlem5  23895  gamigam  23915  lgamcvg2  23917  gamfac  23929  basellem3  23946  basellem8  23951  basellem9  23952  chtprm  24017  logfaclbnd  24087  perfect1  24093  bcp1ctr  24144  bclbnd  24145  bposlem1  24149  lgsdilem  24187  lgsdirnn0  24204  lgsdinn0  24205  lgseisenlem2  24215  lgsquadlem1  24219  2sqlem2  24229  mul2sq  24230  vmadivsum  24257  rpvmasumlem  24262  dchrisumlem1  24264  dchrisumlem2  24265  dchrmusum2  24269  dchrvmasum2if  24272  dchrisum0lem2  24293  logsqvma2  24318  selberg3  24334  selberg4lem1  24335  pntrsumo1  24340  pntrlog2bndlem2  24353  pntrlog2bndlem3  24354  pntrlog2bndlem5  24356  pntibndlem2  24366  pntlemk  24381  pntlemo  24382  ostth2lem4  24411  ostth3  24413  tgbtwndiff  24487  tgifscgr  24490  trgcgrg  24497  motcgr3  24527  tgbtwnconn1lem1  24554  tgbtwnconn1lem2  24555  ismir  24641  miriso  24652  midexlem  24674  ragmir  24682  footex  24700  colperpexlem3  24711  mideulem2  24713  midex  24716  opphllem3  24728  midcgr  24759  lmiisolem  24775  brbtwn2  24872  colinearalglem4  24876  axsegconlem1  24884  axpaschlem  24907  axcontlem4  24934  axcontlem7  24937  axcontlem8  24938  wwlkextwrd  25393  clwwlkn2  25440  clwlkisclwwlklem2a3  25446  clwlkisclwwlk2  25455  clwwlkel  25458  clwwlkfo  25462  clwwlkext2edg  25467  wwlkext2clwwlk  25468  frg2woteq  25725  extwwlkfablem1  25739  clwwlkextfrlem1  25741  numclwlk1lem2foa  25756  numclwlk1lem2fo  25760  numclwlk2lem2f  25768  grpoidinvlem2  25870  gxid  25938  subgores  25969  nvmtri  26237  cnnvm  26251  nvnd  26257  ipidsq  26286  ipnm  26287  ipipcj  26291  blocnilem  26382  ipasslem2  26410  dipsubdir  26426  hvaddsubval  26623  pjhthlem1  26981  pjspansn  27167  pjo  27261  unoplin  27510  adjadj  27526  hmoplin  27532  eigvec1  27552  lnopeqi  27598  nmcexi  27616  lnfnsubi  27636  riesz3i  27652  kbass6  27711  leoprf2  27717  leoprf  27718  pjnmopi  27738  mdslmd1lem1  27915  mdslmd1lem2  27916  superpos  27944  fgreu  28215  resf1o  28260  2sqmod  28355  gsummpt2d  28490  xrge0tsmseq  28497  subrgchr  28504  rhmdvd  28531  symgfcoeu  28555  psgnfzto1stlem  28560  psgnfzto1st  28565  madjusmdetlem2  28601  qtophaus  28610  pstmval  28645  mndpluscn  28679  qqhucn  28743  esumval  28814  gsumesum  28827  esumcst  28831  esumpcvgval  28846  oddpwdc  29134  eulerpartlemgvv  29156  probdif  29200  ballotlemfp1  29271  sgnmul  29360  signsvtn  29420  bnj1415  29794  derangen2  29844  subfaclefac  29846  subfaclim  29858  mrsubrn  30098  sinccvglem  30263  bcprod  30320  filnetlem4  30981  ltflcei  31840  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  poimirlem24  31871  mblfinlem4  31887  ibladdnclem  31905  iblabsnc  31913  iblmulc2nc  31914  ftc1anclem6  31929  ftc1anclem8  31931  sdclem2  31978  ismtycnv  32041  heiborlem10  32059  lflvsass  32559  lkrscss  32576  eqlkr  32577  eqlkr3  32579  ldualvsdi2  32622  omllaw3  32723  cmtcomlemN  32726  cmtbr3N  32732  omlfh3N  32737  llnexchb2lem  33345  dalawlem7  33354  dalawlem11  33358  dalawlem12  33359  pol1N  33387  paddatclN  33426  4atexlemcnd  33549  ltrncoidN  33605  cdleme3b  33707  cdleme11  33748  cdleme15a  33752  cdleme22e  33823  cdleme22g  33827  cdlemg18b  34158  trlcoat  34202  cdlemk2  34311  cdlemk4  34313  cdlemki  34320  cdlemksv2  34326  cdlemk15  34334  cdlemk55a  34438  diainN  34537  dia2dimlem3  34546  dia2dimlem5  34548  dvhlveclem  34588  diaocN  34605  cdlemn4  34678  cdlemn8  34684  dihopelvalcpre  34728  dihmeetlem9N  34795  dih1dimatlem  34809  dihpN  34816  dochvalr3  34843  dochsat  34863  djhjlj  34883  dochdmm1  34890  dihjatcclem4  34901  dihjat1  34909  dihjat4  34913  dochsnkr2cl  34954  dochfl1  34956  lclkrlem2j  34996  mapdordlem2  35117  mapdrvallem2  35125  hdmap10  35323  mzpsubmpt  35497  irrapxlem3  35581  pellexlem6  35591  pell1234qrne0  35612  pell1234qrreccl  35613  pell1234qrmulcl  35614  pell14qrdich  35628  pell1qrgaplem  35632  rmxluc  35697  rmyluc  35698  jm2.24nn  35722  jm2.18  35756  jm2.19lem2  35758  jm2.19lem3  35759  jm2.22  35763  jm2.23  35764  jm2.16nn0  35772  jm2.27c  35775  fnwe2lem2  35822  lmhmfgsplit  35857  hbtlem2  35896  hashgcdeq  35988  relexpmulnn  36214  relexpmulg  36215  int-addassocd  36534  dvconstbi  36596  bccm1k  36604  binomcxplemnotnn0  36618  fmptsnxp  37335  wessf1ornlem  37363  founiiun0  37369  disjinfi  37372  projf1o  37378  lefldiveq  37403  lt4addmuld  37421  fzdifsuc2  37427  suplesup  37459  infrpge  37471  xrlexaddrp  37472  xralrple2  37474  fsumnncl  37534  limcperiod  37591  sumnnodd  37593  limcresiooub  37606  limcresioolb  37607  0ellimcdiv  37613  reclimc  37617  sinmulcos  37623  coskpi2  37624  divcncf  37644  cncfdmsn  37651  cncfiooicclem1  37654  dvmptdiv  37672  fperdvper  37673  dvmptresicc  37674  dvnmptdivc  37696  dvnxpaek  37700  dvnmul  37701  dvnprodlem1  37704  dvnprodlem3  37706  itgcoscmulx  37729  itgsincmulx  37734  itgspltprt  37739  itgiccshift  37740  itgperiod  37741  stoweidlem22  37765  stoweidlem32  37776  wallispilem5  37814  stirlinglem5  37823  dirkertrigeqlem2  37844  dirkertrigeq  37846  dirkercncflem1  37848  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem13  37865  fourierdlem16  37868  fourierdlem19  37871  fourierdlem21  37873  fourierdlem22  37874  fourierdlem28  37880  fourierdlem32  37885  fourierdlem33  37886  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem47  37900  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem56  37909  fourierdlem60  37913  fourierdlem61  37914  fourierdlem64  37917  fourierdlem66  37919  fourierdlem71  37924  fourierdlem73  37926  fourierdlem74  37927  fourierdlem76  37929  fourierdlem78  37931  fourierdlem79  37932  fourierdlem80  37933  fourierdlem81  37934  fourierdlem83  37936  fourierdlem88  37941  fourierdlem92  37945  fourierdlem93  37946  fourierdlem97  37950  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  fourierdlem109  37962  fourierdlem111  37964  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem24  38006  etransclem25  38007  etransclem35  38017  etransclem46  38028  saldifcl2  38051  intsal  38053  sge0sn  38072  sge0ltfirp  38093  sge0iunmptlemre  38108  sge0fodjrnlem  38109  sge0isum  38120  sge0xaddlem1  38126  nnfoctbdjlem  38144  meassle  38152  ismeannd  38156  omeunile  38177  caragendifcl  38186  caratheodory  38200  isomenndlem  38202  ovnsubaddlem1  38239  hoidmv1lelem2  38261  hoidmv1le  38263  hoidmvlelem2  38265  hoidmvle  38269  sigarcol  38287  nn0onn0exALTV  38640  nnsum3primesprm  38698  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  ccats1pfxeq  38775  pfxccatin12lem2  38778  pfxccatin12  38779  c0snmgmhm  39505  rngcifuestrc  39590  funcrngcsetc  39591  funcrngcsetcALT  39592  funcringcsetc  39628  funcringcsetcALTV2lem7  39635  funcringcsetclem7ALTV  39658  lincext3  39842  lincresunit3  39867  nn0onn0ex  39924  nnpw2pmod  39987  blennn0em1  39995  digexp  40011  dignn0ehalf  40021  nn0mulfsum  40028  recsec  40069  reccsc  40070  aacllem  40133