Theorem eqtr2d 2485

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

Syntax hints:   -> wi 4   = wceq 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

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

This theorem is referenced by:  3eqtrrd  2489  3eqtr2rd  2491  ifan  3972  ifor  3973  dfopif  4199  nvocnv  6172  elovmpt3rab1  6521  onsucmin  6641  csbopeq1a  6838  oaabs2  7296  ecinxp  7388  resixpfo  7509  sbthlem3  7631  rankxpsuc  8303  fseqenlem2  8409  dfac2  8514  isf32lem9  8744  compsscnvlem  8753  ttukeylem7  8898  fpwwe2lem11  9021  00id  9758  submul2  10004  mulsubfacd  10023  divadddiv  10266  infmsup  10528  xadd4d  11506  fzdifsuc  11750  fzval3  11867  fzoshftral  11905  ceim1l  11956  fldiv  11969  flmod  11992  intfrac  11993  modcyc2  12014  moddi  12036  uzrdgfni  12051  axdc4uzlem  12074  seqf1olem1  12128  seqf1olem2  12129  seqid2  12135  expnegz  12182  binom2sub  12267  binom3  12269  ccats1swrdeq  12676  swrdccatin12lem2  12696  swrdccatin12  12698  swrdccat3b  12703  cshweqrep  12771  2cshwcshw  12775  ccatco  12783  swrds2  12865  reim  12924  mulre  12936  addcj  12963  absimle  13124  clim2ser  13459  isercoll2  13473  serf0  13485  iseralt  13489  summolem3  13518  isumclim3  13556  mptfzshft  13575  fsumrev  13576  fsum2mul  13586  incexc  13631  isumsplit  13634  mertenslem1  13675  fprodrev  13763  iprodclim3  13775  ef4p  13830  tanval3  13851  efival  13869  sinmul  13889  bitsinvp1  14081  sadaddlem  14098  bitsshft  14107  smu01lem  14117  eulerthlem2  14294  powm2modprm  14310  pythagtriplem16  14336  pczpre  14353  pcqdiv  14363  pcadd  14390  pcfac  14400  prmreclem5  14420  4sqlem10  14447  4sqlem19  14463  vdwapun  14474  vdwlem1  14481  ramcl  14529  strfvd  14645  strfv2d  14646  xpsff1o  14947  xpslem  14952  2oppccomf  15102  oppcepi  15116  sscfn1  15168  sscfn2  15169  invfuc  15322  grpinvssd  16094  grpinvval2  16100  pmtrdifwrdellem2  16486  psgnunilem1  16497  psgnuni  16503  pgp0  16595  sylow1lem1  16597  sylow3lem2  16627  efgredleme  16740  efgcpbllemb  16752  frgpuptinv  16768  frgpup3lem  16774  gexexlem  16837  cyggenod  16866  gsumval3eu  16886  gsumval3OLD  16887  gsumval3  16890  gsumzaddlem  16913  gsumzaddlemOLD  16915  dprd2db  17071  ringinvdv  17322  lss1d  17588  pwssplit1  17684  mplcoe3  18107  mplcoe3OLD  18108  subrgascl  18142  evlseu  18164  ply1sclid  18308  znzrh2  18562  regsumsupp  18636  ipassr2  18660  dsmmfi  18747  frlmlss  18760  frlmip  18787  frlmlbs  18809  frlmup3  18812  islindf4  18851  1marepvmarrepid  19055  madurid  19124  smadiadetlem3  19148  mat2pmatghm  19209  pmatcollpwscmatlem1  19268  pm2mpmhmlem2  19298  cpmadurid  19346  cpmidgsumm2pm  19348  cpmadugsumlemB  19353  cayhamlem2  19363  ntrval2  19530  ordtuni  19669  cnclima  19747  cmpsub  19878  ptbasfi  20060  txbasval  20085  pt1hmeo  20285  alexsubALTlem1  20525  trust  20710  ussid  20741  ressuss  20744  ressprdsds  20852  imasdsf1olem  20854  setsms  20961  tmsxms  20967  tmsxpsmopn  21018  subgnm  21125  tngnm  21143  tngngp2  21144  xrsxmet  21292  xrge0gsumle  21316  metdstri  21333  xrhmeo  21424  lebnumlem3  21441  pcorevlem  21504  pi1xfrcnvlem  21534  clmabs  21560  cvsmuleqdivd  21589  rrxip  21800  rrxds  21803  minveclem4a  21823  pjthlem1  21830  ovolunlem1a  21885  mbfres2  22030  i1faddlem  22078  ibladdlem  22204  iblabs  22213  ditgsplit  22243  dvnres  22312  dveflem  22358  dveq0  22379  dvfsumabs  22402  itgsubstlem  22427  ply1divex  22515  dgrco  22650  plycjlem  22651  taylthlem1  22746  pserdv2  22803  abelthlem6  22809  abelthlem7  22811  tangtx  22876  abssinper  22889  sineq0  22892  explog  22956  reexplog  22957  eflogeq  22964  abslogle  22981  tanarg  22982  logtayl  23019  logtayl2  23021  ang180lem3  23121  affineequiv  23135  affineequiv2  23136  chordthmlem4  23144  chordthmlem5  23145  heron  23147  dcubic1lem  23152  dcubic2  23153  dcubic  23155  mcubic  23156  cubic2  23157  dquartlem1  23160  dquart  23162  quart1lem  23164  quartlem1  23166  quart  23170  acoscos  23202  atanlogaddlem  23222  atantayl2  23247  atantayl3  23248  birthdaylem2  23260  efrlim  23277  amgmlem  23297  logdifbnd  23301  emcllem3  23305  emcllem6  23308  basellem3  23334  basellem8  23339  basellem9  23340  chtprm  23405  logfaclbnd  23475  perfect1  23481  bcp1ctr  23532  bclbnd  23533  bposlem1  23537  lgsdilem  23575  lgsdirnn0  23592  lgsdinn0  23593  lgseisenlem2  23603  lgsquadlem1  23607  2sqlem2  23617  mul2sq  23618  vmadivsum  23645  rpvmasumlem  23650  dchrisumlem1  23652  dchrisumlem2  23653  dchrmusum2  23657  dchrvmasum2if  23660  dchrisum0lem2  23681  logsqvma2  23706  selberg3  23722  selberg4lem1  23723  pntrsumo1  23728  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntibndlem2  23754  pntlemk  23769  pntlemo  23770  ostth2lem4  23799  ostth3  23801  tgcgrextend  23854  tgbtwndiff  23875  tgifscgr  23878  trgcgrg  23884  motcgr3  23910  tgbtwnconn1lem1  23937  tgbtwnconn1lem2  23938  ismir  24018  miriso  24028  midexlem  24047  ragmir  24055  footex  24073  colperpexlem3  24084  mideulem2  24086  midex  24089  opphllem3  24099  midcgr  24124  lmiisolem  24139  brbtwn2  24186  colinearalglem4  24190  axsegconlem1  24198  axpaschlem  24221  axcontlem4  24248  axcontlem7  24251  axcontlem8  24252  wwlkextwrd  24706  clwwlkn2  24753  clwlkisclwwlklem2a3  24759  clwlkisclwwlk2  24768  clwwlkel  24771  clwwlkfo  24775  clwwlkext2edg  24780  wwlkext2clwwlk  24781  frg2woteq  25038  extwwlkfablem1  25052  clwwlkextfrlem1  25054  numclwlk1lem2foa  25069  numclwlk1lem2fo  25073  numclwlk2lem2f  25081  grpoidinvlem2  25185  gxid  25253  subgores  25284  nvmtri  25552  cnnvm  25566  nvnd  25572  ipidsq  25601  ipnm  25602  ipipcj  25606  blocnilem  25697  ipasslem2  25725  dipsubdir  25741  hvaddsubval  25928  pjhthlem1  26287  pjspansn  26473  pjo  26567  unoplin  26817  adjadj  26833  hmoplin  26839  eigvec1  26859  lnopeqi  26905  nmcexi  26923  lnfnsubi  26943  riesz3i  26959  kbass6  27018  leoprf2  27024  leoprf  27025  pjnmopi  27045  mdslmd1lem1  27222  mdslmd1lem2  27223  superpos  27251  fgreu  27491  resf1o  27531  2sqmod  27614  xrge0tsmseq  27755  subrgchr  27762  rhmdvd  27789  qtophaus  27817  pstmval  27852  mndpluscn  27886  qqhucn  27951  esumval  28035  gsumesum  28045  esumcst  28049  esumpcvgval  28062  oddpwdc  28271  eulerpartlemgvv  28293  probdif  28337  ballotlemfp1  28408  sgnmul  28459  signsvtn  28519  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem4  28552  lgamgulmlem5  28553  gamigam  28573  lgamcvg2  28575  gamfac  28587  derangen2  28596  subfaclefac  28598  subfaclim  28610  mrsubrn  28851  sinccvglem  29016  binomfallfaclem2  29138  ltflcei  30019  mblfinlem4  30030  ibladdnclem  30047  iblabsnc  30055  iblmulc2nc  30056  ftc1anclem6  30071  ftc1anclem8  30073  filnetlem4  30175  sdclem2  30211  ismtycnv  30274  heiborlem10  30292  mzpsubmpt  30651  irrapxlem3  30736  pellexlem6  30746  pell1234qrne0  30765  pell1234qrreccl  30766  pell1234qrmulcl  30767  pell14qrdich  30781  pell1qrgaplem  30785  rmxluc  30848  rmyluc  30849  jm2.24nn  30873  jm2.18  30906  jm2.19lem2  30908  jm2.19lem3  30909  jm2.22  30913  jm2.23  30914  jm2.16nn0  30922  jm2.27c  30925  fnwe2lem2  30973  lmhmfgsplit  31008  hbtlem2  31049  hashgcdeq  31134  lcmgcdlem  31188  dvconstbi  31215  fmptsnxp  31398  lefldiveq  31436  lt4addmuld  31460  fzdifsuc2  31466  fsumnncl  31526  limcperiod  31588  sumnnodd  31590  limcresiooub  31602  limcresioolb  31603  0ellimcdiv  31609  reclimc  31613  sinmulcos  31619  coskpi2  31620  divcncf  31640  cncfdmsn  31647  cncfiooicclem1  31650  dvmptdiv  31668  fperdvper  31669  dvmptresicc  31670  dvnmptdivc  31689  dvnxpaek  31693  dvnmul  31694  dvnprodlem1  31697  dvnprodlem3  31699  itgcoscmulx  31722  itgsincmulx  31727  itgspltprt  31732  itgiccshift  31733  itgperiod  31734  stoweidlem22  31758  stoweidlem32  31768  wallispilem5  31805  stirlinglem5  31814  dirkertrigeqlem2  31835  dirkertrigeq  31837  dirkercncflem1  31839  dirkercncflem2  31840  dirkercncflem4  31842  fourierdlem13  31856  fourierdlem16  31859  fourierdlem19  31862  fourierdlem21  31864  fourierdlem22  31865  fourierdlem28  31871  fourierdlem32  31875  fourierdlem33  31876  fourierdlem42  31885  fourierdlem47  31890  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem56  31899  fourierdlem60  31903  fourierdlem61  31904  fourierdlem64  31907  fourierdlem66  31909  fourierdlem71  31914  fourierdlem73  31916  fourierdlem74  31917  fourierdlem76  31919  fourierdlem78  31921  fourierdlem79  31922  fourierdlem80  31923  fourierdlem81  31924  fourierdlem83  31926  fourierdlem88  31931  fourierdlem92  31935  fourierdlem93  31936  fourierdlem97  31940  fourierdlem101  31944  fourierdlem103  31946  fourierdlem104  31947  fourierdlem109  31952  fourierdlem111  31954  fouriersw  31968  elaa2lem  31970  etransclem24  31995  etransclem25  31996  etransclem28  31999  etransclem46  32017  sigarcol  32035  funcestrcsetclem7  32618  funcsetcestrclem7  32633  rngcifuestrc  32680  funcrngcsetc  32681  funcrngcsetcALT  32682  funcringcsetc  32715  funcringcsetcOLD2lem7  32722  funcringcsetclem7OLD  32745  lincext3  32927  lincresunit3  32952  recsec  33020  reccsc  33021  bnj1415  33962  lflvsass  34681  lkrscss  34698  eqlkr  34699  eqlkr3  34701  ldualvsdi2  34744  omllaw3  34845  cmtcomlemN  34848  cmtbr3N  34854  omlfh3N  34859  llnexchb2lem  35467  dalawlem7  35476  dalawlem11  35480  dalawlem12  35481  pol1N  35509  paddatclN  35548  4atexlemcnd  35671  ltrncoidN  35727  cdleme3b  35829  cdleme11  35870  cdleme15a  35874  cdleme22e  35945  cdleme22g  35949  cdlemg18b  36280  trlcoat  36324  cdlemk2  36433  cdlemk4  36435  cdlemki  36442  cdlemksv2  36448  cdlemk15  36456  cdlemk55a  36560  diainN  36659  dia2dimlem3  36668  dia2dimlem5  36670  dvhlveclem  36710  diaocN  36727  cdlemn4  36800  cdlemn8  36806  dihopelvalcpre  36850  dihmeetlem9N  36917  dih1dimatlem  36931  dihpN  36938  dochvalr3  36965  dochsat  36985  djhjlj  37005  dochdmm1  37012  dihjatcclem4  37023  dihjat1  37031  dihjat4  37035  dochsnkr2cl  37076  dochfl1  37078  lclkrlem2j  37118  mapdordlem2  37239  mapdrvallem2  37247  hdmap10  37445