Theorem eqtr2d 2657

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

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  3eqtrrd  2661  3eqtr2rd  2663  ifan  4134  ifor  4135  dfopif  4399  nvocnv  6537  elovmpt3rab1  6893  onsucmin  7021  csbopeq1a  7221  oaabs2  7725  ecinxp  7822  resixpfo  7946  sbthlem3  8072  rankxpsuc  8745  fseqenlem2  8848  dfac2  8953  isf32lem9  9183  compsscnvlem  9192  ttukeylem7  9337  fpwwe2lem11  9462  00id  10211  submul2  10470  mulsubfacd  10492  divadddiv  10740  infrenegsup  11006  xadd4d  12133  fzdifsuc  12400  fzval3  12536  fzoshftral  12585  ceim1l  12646  fldiv  12659  flmod  12684  intfrac  12685  modcyc2  12706  moddi  12738  uzrdgfni  12757  axdc4uzlem  12782  seqf1olem1  12840  seqf1olem2  12841  seqid2  12847  expnegz  12894  binom2sub  12981  binom3  12985  hashreshashfun  13226  wrdlenccats1lenm1  13399  ccatw2s1p2  13414  ccats1swrdeq  13469  swrdccatin12lem2  13489  swrdccatin12  13491  swrdccat3b  13496  cshweqrep  13567  2cshwcshw  13571  ccatco  13581  swrds2  13685  relexpsucnnr  13765  relexpaddnn  13791  reim  13849  mulre  13861  addcj  13888  absimle  14049  clim2ser  14385  isercoll2  14399  serf0  14411  iseralt  14415  summolem3  14445  isumclim3  14490  mptfzshft  14510  fsumrev  14511  fsum2mul  14521  incexc  14569  isumsplit  14572  mertenslem1  14616  fprodrev  14707  iprodclim3  14731  binomfallfaclem2  14771  ef4p  14843  tanval3  14864  efival  14882  sinmul  14902  bitsinvp1  15171  sadaddlem  15188  bitsshft  15197  smu01lem  15207  dfgcd2  15263  lcmgcdlem  15319  lcm1  15323  lcmfass  15359  eulerthlem2  15487  hashgcdeq  15494  powm2modprm  15508  pythagtriplem16  15535  pczpre  15552  pcqdiv  15562  pcadd  15593  pcfac  15603  prmreclem5  15624  4sqlem10  15651  4sqlem19  15667  vdwapun  15678  vdwlem1  15685  ramcl  15733  setsstruct  15898  strfvd  15904  strfv2d  15905  xpsff1o  16228  xpslem  16233  2oppccomf  16385  oppcepi  16399  sscfn1  16477  sscfn2  16478  invfuc  16634  funcestrcsetclem7  16786  funcsetcestrclem7  16801  grpinvssd  17492  grpinvval2  17498  pmtrdifwrdellem2  17902  psgnunilem1  17913  psgnuni  17919  pgp0  18011  sylow1lem1  18013  sylow3lem2  18043  efgredleme  18156  efgcpbllemb  18168  frgpuptinv  18184  frgpup3lem  18190  gexexlem  18255  cyggenod  18286  gsumval3eu  18305  gsumval3  18308  gsumzaddlem  18321  dprd2db  18442  ringinvdv  18694  lss1d  18963  pwssplit1  19059  mplcoe3  19466  subrgascl  19498  evlseu  19516  ply1sclid  19658  znzrh2  19894  regsumsupp  19968  ipassr2  19992  dsmmfi  20082  frlmlss  20095  frlmip  20117  frlmlbs  20136  frlmup3  20139  islindf4  20177  1marepvmarrepid  20381  madurid  20450  smadiadetlem3  20474  mat2pmatghm  20535  pmatcollpwscmatlem1  20594  pm2mpmhmlem2  20624  cpmadurid  20672  cpmidgsumm2pm  20674  cpmadugsumlemB  20679  cayhamlem2  20689  ntrval2  20855  ordtuni  20994  cnclima  21072  cmpsub  21203  ptbasfi  21384  txbasval  21409  pt1hmeo  21609  alexsubALTlem1  21851  trust  22033  ussid  22064  ressuss  22067  ressprdsds  22176  imasdsf1olem  22178  setsms  22285  tmsxms  22291  tmsxpsmopn  22342  subgnm  22437  tngnm  22455  tngngp2  22456  xrsxmet  22612  xrge0gsumle  22636  metdstri  22654  xrhmeo  22745  lebnumlem3  22762  pcorevlem  22826  pi1xfrcnvlem  22856  clmabs  22883  cvsmuleqdivd  22934  rrxip  23178  rrxds  23181  minveclem4a  23201  pjthlem1  23208  divcncf  23216  ovolunlem1a  23264  mbfres2  23412  i1faddlem  23460  ibladdlem  23586  iblabs  23595  ditgsplit  23625  dvnres  23694  dvmptdiv  23737  dveflem  23742  dveq0  23763  dvfsumabs  23786  itgsubstlem  23811  ply1divex  23896  dgrco  24031  plycjlem  24032  taylthlem1  24127  pserdv2  24184  abelthlem6  24190  abelthlem7  24192  tangtx  24257  abssinper  24270  sineq0  24273  explog  24340  reexplog  24341  eflogeq  24348  abslogle  24364  tanarg  24365  logtayl  24406  logtayl2  24408  relogbdiv  24517  ang180lem3  24541  affineequiv  24553  affineequiv2  24554  chordthmlem4  24562  chordthmlem5  24563  heron  24565  dcubic1lem  24570  dcubic2  24571  dcubic  24573  mcubic  24574  cubic2  24575  dquartlem1  24578  dquart  24580  quart1lem  24582  quartlem1  24584  quart  24588  acoscos  24620  atanlogaddlem  24640  atantayl2  24665  atantayl3  24666  birthdaylem2  24679  efrlim  24696  amgmlem  24716  logdifbnd  24720  emcllem3  24724  emcllem6  24727  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  gamigam  24779  lgamcvg2  24781  gamfac  24793  basellem3  24809  basellem8  24814  basellem9  24815  chtprm  24879  logfaclbnd  24947  perfect1  24953  bcp1ctr  25004  bclbnd  25005  bposlem1  25009  lgsdilem  25049  lgsdirnn0  25069  lgsdinn0  25070  gausslemma2dlem1a  25090  gausslemma2dlem4  25094  gausslemma2dlem5a  25095  lgseisenlem2  25101  lgsquadlem1  25105  2sqlem2  25143  mul2sq  25144  vmadivsum  25171  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasum2if  25186  dchrisum0lem2  25207  logsqvma2  25232  selberg3  25248  selberg4lem1  25249  pntrsumo1  25254  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntibndlem2  25280  pntlemk  25295  pntlemo  25296  ostth2lem4  25325  ostth3  25327  tgbtwndiff  25401  tgifscgr  25403  trgcgrg  25410  motcgr3  25440  tgbtwnconn1lem1  25467  tgbtwnconn1lem2  25468  ismir  25554  miriso  25565  midexlem  25587  ragmir  25595  footex  25613  colperpexlem3  25624  mideulem2  25626  midex  25629  opphllem3  25641  midcgr  25672  lmiisolem  25688  brbtwn2  25785  colinearalglem4  25789  axsegconlem1  25797  axpaschlem  25820  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  ushgredgedgloop  26123  crctcshwlkn0lem6  26707  wwlksnextwrd  26792  clwlkclwwlklem2a3  26895  clwlkclwwlk2  26904  clwwlksel  26914  clwwlksfo  26918  clwwlksext2edg  26923  wwlksext2clwwlk  26924  eupth2eucrct  27077  clwwlkextfrlem1  27208  numclwlk1lem2fo  27228  numclwlk2lem2f  27236  grpoidinvlem2  27359  nvmtri  27526  cnnvm  27537  nvnd  27543  ipidsq  27565  ipnm  27566  ipipcj  27570  blocnilem  27659  ipasslem2  27687  dipsubdir  27703  hvaddsubval  27890  pjhthlem1  28250  pjspansn  28436  pjo  28530  unoplin  28779  adjadj  28795  hmoplin  28801  eigvec1  28821  lnopeqi  28867  nmcexi  28885  lnfnsubi  28905  riesz3i  28921  kbass6  28980  leoprf2  28986  leoprf  28987  pjnmopi  29007  mdslmd1lem1  29184  mdslmd1lem2  29185  superpos  29213  ifeq3da  29365  fgreu  29471  resf1o  29505  fprodex01  29571  2sqmod  29648  gsummpt2d  29781  xrge0tsmseq  29787  subrgchr  29794  rhmdvd  29821  symgfcoeu  29845  psgnfzto1stlem  29850  psgnfzto1st  29855  madjusmdetlem2  29894  qtophaus  29903  pstmval  29938  mndpluscn  29972  qqhucn  30036  esumval  30108  gsumesum  30121  esumcst  30125  esumpcvgval  30140  oddpwdc  30416  eulerpartlemgvv  30438  probdif  30482  sgnmul  30604  signsvtn  30661  actfunsnf1o  30682  reprpmtf1o  30704  hgt750lemd  30726  logdivsqrle  30728  hgt750lemg  30732  hgt750lemb  30734  bnj1415  31106  derangen2  31156  subfaclefac  31158  subfaclim  31170  mrsubrn  31410  sinccvglem  31566  bcprod  31624  filnetlem4  32376  curunc  33391  ltflcei  33397  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  mblfinlem4  33449  ibladdnclem  33466  iblabsnc  33474  iblmulc2nc  33475  ftc1anclem6  33490  ftc1anclem8  33492  sdclem2  33538  ismtycnv  33601  heiborlem10  33619  lflvsass  34368  lkrscss  34385  eqlkr  34386  eqlkr3  34388  ldualvsdi2  34431  omllaw3  34532  cmtcomlemN  34535  cmtbr3N  34541  omlfh3N  34546  llnexchb2lem  35154  dalawlem7  35163  dalawlem11  35167  dalawlem12  35168  pol1N  35196  paddatclN  35235  4atexlemcnd  35358  ltrncoidN  35414  cdleme3b  35516  cdleme11  35557  cdleme15a  35561  cdleme22e  35632  cdleme22g  35636  cdlemg18b  35967  trlcoat  36011  cdlemk2  36120  cdlemk4  36122  cdlemki  36129  cdlemksv2  36135  cdlemk15  36143  cdlemk55a  36247  diainN  36346  dia2dimlem3  36355  dia2dimlem5  36357  dvhlveclem  36397  diaocN  36414  cdlemn4  36487  cdlemn8  36493  dihopelvalcpre  36537  dihmeetlem9N  36604  dih1dimatlem  36618  dihpN  36625  dochvalr3  36652  dochsat  36672  djhjlj  36692  dochdmm1  36699  dihjatcclem4  36710  dihjat1  36718  dihjat4  36722  dochsnkr2cl  36763  dochfl1  36765  lclkrlem2j  36805  mapdordlem2  36926  mapdrvallem2  36934  hdmap10  37132  mzpsubmpt  37306  irrapxlem3  37388  pellexlem6  37398  pell1234qrne0  37417  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell14qrdich  37433  pell1qrgaplem  37437  rmxluc  37501  rmyluc  37502  jm2.24nn  37526  jm2.18  37555  jm2.19lem2  37557  jm2.19lem3  37558  jm2.22  37562  jm2.23  37563  jm2.16nn0  37571  jm2.27c  37574  fnwe2lem2  37621  lmhmfgsplit  37656  hbtlem2  37694  relexpmulnn  38001  relexpmulg  38002  ntrclsneine0lem  38362  int-addassocd  38477  dvconstbi  38533  bccm1k  38541  binomcxplemnotnn0  38555  fmptsnxp  39349  wessf1ornlem  39371  founiiun0  39377  disjinfi  39380  projf1o  39386  infnsuprnmpt  39465  lefldiveq  39505  lt4addmuld  39520  fzdifsuc2  39525  suplesup  39555  infrpge  39567  xrlexaddrp  39568  xralrple2  39570  infleinflem1  39586  supminfrnmpt  39672  supminfxr2  39699  fsumnncl  39803  limcperiod  39860  sumnnodd  39862  limcresiooub  39874  limcresioolb  39875  0ellimcdiv  39881  reclimc  39885  limsupval3  39924  limsupequzmpt2  39950  liminfval5  39997  limsupresxr  39998  liminfresxr  39999  liminfvalxr  40015  liminfequzmpt2  40023  climliminflimsupd  40033  liminfltlem  40036  sinmulcos  40076  coskpi2  40077  cncfdmsn  40103  cncfiooicclem1  40106  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  fperdvper  40133  dvmptresicc  40134  dvnmptdivc  40153  dvnxpaek  40157  dvnmul  40158  dvnprodlem1  40161  dvnprodlem3  40163  itgcoscmulx  40185  itgsincmulx  40190  itgspltprt  40195  itgiccshift  40196  itgperiod  40197  sublevolico  40201  volioof  40204  ovolsplit  40205  fvvolioof  40206  fvvolicof  40208  stoweidlem22  40239  stoweidlem32  40249  wallispilem5  40286  stirlinglem5  40295  dirkertrigeqlem2  40316  dirkertrigeq  40318  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem13  40337  fourierdlem16  40340  fourierdlem19  40343  fourierdlem21  40345  fourierdlem22  40346  fourierdlem28  40352  fourierdlem32  40356  fourierdlem33  40357  fourierdlem42  40366  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem56  40379  fourierdlem60  40383  fourierdlem61  40384  fourierdlem64  40387  fourierdlem66  40389  fourierdlem71  40394  fourierdlem73  40396  fourierdlem74  40397  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem80  40403  fourierdlem81  40404  fourierdlem83  40406  fourierdlem88  40411  fourierdlem92  40415  fourierdlem93  40416  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem109  40432  fourierdlem111  40434  fouriersw  40448  elaa2lem  40450  etransclem24  40475  etransclem25  40476  etransclem35  40486  etransclem46  40497  rrxdsfi  40505  rrndistlt  40510  rrxunitopnfi  40512  qndenserrnbl  40515  qndenserrnopnlem  40517  saldifcl2  40546  intsal  40548  sge0sn  40596  sge0ltfirp  40617  sge0iunmptlemre  40632  sge0fodjrnlem  40633  sge0isum  40644  sge0xaddlem1  40650  nnfoctbdjlem  40672  meassle  40680  ismeannd  40684  meadif  40696  meaiuninclem  40697  meaiininclem  40700  omeunile  40719  caragendifcl  40728  caratheodory  40742  isomenndlem  40744  ovnsubaddlem1  40784  hoidmv1lelem2  40806  hoidmv1le  40808  hoidmvlelem2  40810  hoidmvle  40814  hoi2toco  40821  rrnmbl  40828  hoidifhspdmvle  40834  voncmpl  40835  hoiqssbl  40839  hspmbllem1  40840  hspmbllem2  40841  ovolval2lem  40857  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  hoimbl2  40879  vonhoire  40886  salpreimagelt  40918  salpreimalegt  40920  preimaioomnf  40929  smfres  40997  smfmullem1  40998  smflimmpt  41016  smfsupmpt  41021  smfinfmpt  41025  smflimsupmpt  41035  smfliminflem  41036  smfliminfmpt  41038  sigarcol  41053  ccats1pfxeq  41421  pfxccatin12lem2  41424  pfxccatin12  41425  sfprmdvdsmersenne  41520  lighneallem3  41524  lighneallem4  41527  nn0onn0exALTV  41609  nnsum3primesprm  41678  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  elsprel  41725  c0snmgmhm  41914  rngcifuestrc  41997  funcrngcsetc  41998  funcrngcsetcALT  41999  funcringcsetc  42035  funcringcsetcALTV2lem7  42042  funcringcsetclem7ALTV  42065  lincext3  42245  lincresunit3  42270  nn0onn0ex  42318  nnpw2pmod  42377  blennn0em1  42385  digexp  42401  dignn0ehalf  42411  nn0mulfsum  42418  recsec  42497  reccsc  42498  aacllem  42547  amgmlemALT  42549