Theorem eqtr2d 2497

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

Syntax hints:   -> wi 4   = wceq 1455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-cleq 2455

This theorem is referenced by:  3eqtrrd  2501  3eqtr2rd  2503  ifan  3939  ifor  3940  dfopif  4177  nvocnv  6205  elovmpt3rab1  6554  onsucmin  6675  csbopeq1a  6873  oaabs2  7372  ecinxp  7464  resixpfo  7586  sbthlem3  7710  rankxpsuc  8379  fseqenlem2  8482  dfac2  8587  isf32lem9  8817  compsscnvlem  8826  ttukeylem7  8971  fpwwe2lem11  9091  00id  9834  submul2  10087  mulsubfacd  10106  divadddiv  10350  infrenegsup  10619  infmsupOLD  10620  xadd4d  11618  fzdifsuc  11884  fzval3  12014  fzoshftral  12053  ceim1l  12106  fldiv  12119  flmod  12143  intfrac  12144  modcyc2  12165  moddi  12189  uzrdgfni  12204  axdc4uzlem  12227  seqf1olem1  12284  seqf1olem2  12285  seqid2  12291  expnegz  12338  binom2sub  12423  binom3  12425  wrdlenccats1lenm1  12793  ccatw2s1p2  12807  ccats1swrdeq  12862  swrdccatin12lem2  12882  swrdccatin12  12884  swrdccat3b  12889  cshweqrep  12957  2cshwcshw  12961  ccatco  12969  swrds2  13066  relexpsucnnr  13137  relexpaddnn  13163  reim  13221  mulre  13233  addcj  13260  absimle  13421  clim2ser  13767  isercoll2  13781  serf0  13796  iseralt  13800  summolem3  13829  isumclim3  13869  mptfzshft  13888  fsumrev  13889  fsum2mul  13899  incexc  13944  isumsplit  13947  mertenslem1  13989  fprodrev  14080  iprodclim3  14102  binomfallfaclem2  14142  ef4p  14216  tanval3  14237  efival  14255  sinmul  14275  bitsinvp1  14472  sadaddlem  14489  bitsshft  14498  smu01lem  14508  lcmgcdlem  14620  lcm1  14624  lcmfass  14668  eulerthlem2  14779  powm2modprm  14803  pythagtriplem16  14829  pczpre  14846  pcqdiv  14856  pcadd  14883  pcfac  14893  prmreclem5  14913  4sqlem10  14940  4sqlem19  14962  vdwapun  14973  vdwlem1  14980  ramcl  15036  strfvd  15203  strfv2d  15204  xpsff1o  15523  xpslem  15528  2oppccomf  15679  oppcepi  15693  sscfn1  15771  sscfn2  15772  invfuc  15928  funcestrcsetclem7  16080  funcsetcestrclem7  16095  grpinvssd  16780  grpinvval2  16786  pmtrdifwrdellem2  17172  psgnunilem1  17183  psgnuni  17189  pgp0  17297  sylow1lem1  17299  sylow3lem2  17329  efgredleme  17442  efgcpbllemb  17454  frgpuptinv  17470  frgpup3lem  17476  gexexlem  17539  cyggenod  17568  gsumval3eu  17587  gsumval3  17590  gsumzaddlem  17603  dprd2db  17725  ringinvdv  17971  lss1d  18235  pwssplit1  18331  mplcoe3  18739  subrgascl  18770  evlseu  18788  ply1sclid  18930  znzrh2  19165  regsumsupp  19239  ipassr2  19263  dsmmfi  19350  frlmlss  19363  frlmip  19385  frlmlbs  19404  frlmup3  19407  islindf4  19445  1marepvmarrepid  19649  madurid  19718  smadiadetlem3  19742  mat2pmatghm  19803  pmatcollpwscmatlem1  19862  pm2mpmhmlem2  19892  cpmadurid  19940  cpmidgsumm2pm  19942  cpmadugsumlemB  19947  cayhamlem2  19957  ntrval2  20115  ordtuni  20255  cnclima  20333  cmpsub  20464  ptbasfi  20645  txbasval  20670  pt1hmeo  20870  alexsubALTlem1  21111  trust  21293  ussid  21324  ressuss  21327  ressprdsds  21435  imasdsf1olem  21437  setsms  21544  tmsxms  21550  tmsxpsmopn  21601  subgnm  21690  tngnm  21708  tngngp2  21709  xrsxmet  21876  xrge0gsumle  21900  metdstri  21917  metdstriOLD  21932  xrhmeo  22023  lebnumlem3  22040  lebnumlem3OLD  22043  pcorevlem  22106  pi1xfrcnvlem  22136  clmabs  22162  cvsmuleqdivd  22191  rrxip  22398  rrxds  22401  minveclem4a  22421  minveclem4aOLD  22433  pjthlem1  22440  ovolunlem1a  22498  mbfres2  22650  i1faddlem  22700  ibladdlem  22826  iblabs  22835  ditgsplit  22865  dvnres  22934  dveflem  22980  dveq0  23001  dvfsumabs  23024  itgsubstlem  23049  ply1divex  23136  dgrco  23278  plycjlem  23279  taylthlem1  23377  pserdv2  23434  abelthlem6  23440  abelthlem7  23442  tangtx  23509  abssinper  23522  sineq0  23525  explog  23592  reexplog  23593  eflogeq  23600  abslogle  23616  tanarg  23617  logtayl  23654  logtayl2  23656  relogbdiv  23765  ang180lem3  23789  affineequiv  23801  affineequiv2  23802  chordthmlem4  23810  chordthmlem5  23811  heron  23813  dcubic1lem  23818  dcubic2  23819  dcubic  23821  mcubic  23822  cubic2  23823  dquartlem1  23826  dquart  23828  quart1lem  23830  quartlem1  23832  quart  23836  acoscos  23868  atanlogaddlem  23888  atantayl2  23913  atantayl3  23914  birthdaylem2  23927  efrlim  23944  amgmlem  23964  logdifbnd  23968  emcllem3  23972  emcllem6  23975  lgamgulmlem2  24004  lgamgulmlem3  24005  lgamgulmlem4  24006  lgamgulmlem5  24007  gamigam  24027  lgamcvg2  24029  gamfac  24041  basellem3  24058  basellem8  24063  basellem9  24064  chtprm  24129  logfaclbnd  24199  perfect1  24205  bcp1ctr  24256  bclbnd  24257  bposlem1  24261  lgsdilem  24299  lgsdirnn0  24316  lgsdinn0  24317  lgseisenlem2  24327  lgsquadlem1  24331  2sqlem2  24341  mul2sq  24342  vmadivsum  24369  rpvmasumlem  24374  dchrisumlem1  24376  dchrisumlem2  24377  dchrmusum2  24381  dchrvmasum2if  24384  dchrisum0lem2  24405  logsqvma2  24430  selberg3  24446  selberg4lem1  24447  pntrsumo1  24452  pntrlog2bndlem2  24465  pntrlog2bndlem3  24466  pntrlog2bndlem5  24468  pntibndlem2  24478  pntlemk  24493  pntlemo  24494  ostth2lem4  24523  ostth3  24525  tgbtwndiff  24599  tgifscgr  24602  trgcgrg  24609  motcgr3  24639  tgbtwnconn1lem1  24666  tgbtwnconn1lem2  24667  ismir  24753  miriso  24764  midexlem  24786  ragmir  24794  footex  24812  colperpexlem3  24823  mideulem2  24825  midex  24828  opphllem3  24840  midcgr  24871  lmiisolem  24887  brbtwn2  24984  colinearalglem4  24988  axsegconlem1  24996  axpaschlem  25019  axcontlem4  25046  axcontlem7  25049  axcontlem8  25050  wwlkextwrd  25505  clwwlkn2  25552  clwlkisclwwlklem2a3  25558  clwlkisclwwlk2  25567  clwwlkel  25570  clwwlkfo  25574  clwwlkext2edg  25579  wwlkext2clwwlk  25580  frg2woteq  25837  extwwlkfablem1  25851  clwwlkextfrlem1  25853  numclwlk1lem2foa  25868  numclwlk1lem2fo  25872  numclwlk2lem2f  25880  grpoidinvlem2  25982  gxid  26050  subgores  26081  nvmtri  26349  cnnvm  26363  nvnd  26369  ipidsq  26398  ipnm  26399  ipipcj  26403  blocnilem  26494  ipasslem2  26522  dipsubdir  26538  hvaddsubval  26735  pjhthlem1  27093  pjspansn  27279  pjo  27373  unoplin  27622  adjadj  27638  hmoplin  27644  eigvec1  27664  lnopeqi  27710  nmcexi  27728  lnfnsubi  27748  riesz3i  27764  kbass6  27823  leoprf2  27829  leoprf  27830  pjnmopi  27850  mdslmd1lem1  28027  mdslmd1lem2  28028  superpos  28056  fgreu  28323  resf1o  28364  2sqmod  28458  gsummpt2d  28593  xrge0tsmseq  28599  subrgchr  28606  rhmdvd  28633  symgfcoeu  28657  psgnfzto1stlem  28662  psgnfzto1st  28667  madjusmdetlem2  28703  qtophaus  28712  pstmval  28747  mndpluscn  28781  qqhucn  28845  esumval  28916  gsumesum  28929  esumcst  28933  esumpcvgval  28948  oddpwdc  29236  eulerpartlemgvv  29258  probdif  29302  ballotlemfp1  29373  sgnmul  29462  signsvtn  29522  bnj1415  29896  derangen2  29946  subfaclefac  29948  subfaclim  29960  mrsubrn  30200  sinccvglem  30365  bcprod  30423  filnetlem4  31086  ltflcei  31978  poimirlem16  32001  poimirlem17  32002  poimirlem19  32004  poimirlem20  32005  poimirlem24  32009  mblfinlem4  32025  ibladdnclem  32043  iblabsnc  32051  iblmulc2nc  32052  ftc1anclem6  32067  ftc1anclem8  32069  sdclem2  32116  ismtycnv  32179  heiborlem10  32197  lflvsass  32692  lkrscss  32709  eqlkr  32710  eqlkr3  32712  ldualvsdi2  32755  omllaw3  32856  cmtcomlemN  32859  cmtbr3N  32865  omlfh3N  32870  llnexchb2lem  33478  dalawlem7  33487  dalawlem11  33491  dalawlem12  33492  pol1N  33520  paddatclN  33559  4atexlemcnd  33682  ltrncoidN  33738  cdleme3b  33840  cdleme11  33881  cdleme15a  33885  cdleme22e  33956  cdleme22g  33960  cdlemg18b  34291  trlcoat  34335  cdlemk2  34444  cdlemk4  34446  cdlemki  34453  cdlemksv2  34459  cdlemk15  34467  cdlemk55a  34571  diainN  34670  dia2dimlem3  34679  dia2dimlem5  34681  dvhlveclem  34721  diaocN  34738  cdlemn4  34811  cdlemn8  34817  dihopelvalcpre  34861  dihmeetlem9N  34928  dih1dimatlem  34942  dihpN  34949  dochvalr3  34976  dochsat  34996  djhjlj  35016  dochdmm1  35023  dihjatcclem4  35034  dihjat1  35042  dihjat4  35046  dochsnkr2cl  35087  dochfl1  35089  lclkrlem2j  35129  mapdordlem2  35250  mapdrvallem2  35258  hdmap10  35456  mzpsubmpt  35630  irrapxlem3  35713  pellexlem6  35723  pell1234qrne0  35744  pell1234qrreccl  35745  pell1234qrmulcl  35746  pell14qrdich  35760  pell1qrgaplem  35764  rmxluc  35829  rmyluc  35830  jm2.24nn  35854  jm2.18  35888  jm2.19lem2  35890  jm2.19lem3  35891  jm2.22  35895  jm2.23  35896  jm2.16nn0  35904  jm2.27c  35907  fnwe2lem2  35954  lmhmfgsplit  35989  hbtlem2  36028  hashgcdeq  36120  relexpmulnn  36346  relexpmulg  36347  int-addassocd  36665  dvconstbi  36727  bccm1k  36735  binomcxplemnotnn0  36749  fmptsnxp  37470  wessf1ornlem  37497  founiiun0  37503  disjinfi  37506  projf1o  37512  lefldiveq  37544  lt4addmuld  37562  fzdifsuc2  37568  suplesup  37600  infrpge  37612  xrlexaddrp  37613  xralrple2  37615  fsumnncl  37688  limcperiod  37746  sumnnodd  37748  limcresiooub  37761  limcresioolb  37762  0ellimcdiv  37768  reclimc  37772  sinmulcos  37778  coskpi2  37779  divcncf  37799  cncfdmsn  37806  cncfiooicclem1  37809  dvmptdiv  37827  fperdvper  37828  dvmptresicc  37829  dvnmptdivc  37851  dvnxpaek  37855  dvnmul  37856  dvnprodlem1  37859  dvnprodlem3  37861  itgcoscmulx  37884  itgsincmulx  37889  itgspltprt  37894  itgiccshift  37895  itgperiod  37896  stoweidlem22  37920  stoweidlem32  37931  wallispilem5  37969  stirlinglem5  37978  dirkertrigeqlem2  37999  dirkertrigeq  38001  dirkercncflem1  38003  dirkercncflem2  38004  dirkercncflem4  38006  fourierdlem13  38020  fourierdlem16  38023  fourierdlem19  38026  fourierdlem21  38028  fourierdlem22  38029  fourierdlem28  38035  fourierdlem32  38040  fourierdlem33  38041  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem47  38055  fourierdlem48  38056  fourierdlem49  38057  fourierdlem50  38058  fourierdlem56  38064  fourierdlem60  38068  fourierdlem61  38069  fourierdlem64  38072  fourierdlem66  38074  fourierdlem71  38079  fourierdlem73  38081  fourierdlem74  38082  fourierdlem76  38084  fourierdlem78  38086  fourierdlem79  38087  fourierdlem80  38088  fourierdlem81  38089  fourierdlem83  38091  fourierdlem88  38096  fourierdlem92  38100  fourierdlem93  38101  fourierdlem97  38105  fourierdlem101  38109  fourierdlem103  38111  fourierdlem104  38112  fourierdlem109  38117  fourierdlem111  38119  fouriersw  38133  elaa2lem  38135  elaa2lemOLD  38136  etransclem24  38161  etransclem25  38162  etransclem35  38172  etransclem46  38183  rrxdsfi  38192  rrndistlt  38197  rrxunitopnfi  38199  qndenserrnbl  38202  qndenserrnopnlem  38204  saldifcl2  38225  intsal  38227  sge0sn  38259  sge0ltfirp  38280  sge0iunmptlemre  38295  sge0fodjrnlem  38296  sge0isum  38307  sge0xaddlem1  38313  nnfoctbdjlem  38331  meassle  38339  ismeannd  38343  omeunile  38364  caragendifcl  38373  caratheodory  38387  isomenndlem  38389  ovnsubaddlem1  38430  hoidmv1lelem2  38452  hoidmv1le  38454  hoidmvlelem2  38456  hoidmvle  38460  hoi2toco  38467  rrnmbl  38474  hoidifhspdmvle  38480  voncmpl  38481  hoiqssbl  38485  hspmbllem1  38486  hspmbllem2  38487  sigarcol  38511  nn0onn0exALTV  38865  nnsum3primesprm  38923  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  ccats1pfxeq  39002  pfxccatin12lem2  39005  pfxccatin12  39006  ushgredgedgaloop  39358  c0snmgmhm  40187  rngcifuestrc  40272  funcrngcsetc  40273  funcrngcsetcALT  40274  funcringcsetc  40310  funcringcsetcALTV2lem7  40317  funcringcsetclem7ALTV  40340  lincext3  40522  lincresunit3  40547  nn0onn0ex  40604  nnpw2pmod  40667  blennn0em1  40675  digexp  40691  dignn0ehalf  40701  nn0mulfsum  40708  recsec  40749  reccsc  40750  aacllem  40813