Theorem eqtr2d 2437

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

Syntax hints:   -> wi 4   = wceq 1649

This theorem is referenced by:  3eqtrrd  2441  3eqtr2rd  2443  ifan  3738  ifor  3739  dfopif  3941  onsucmin  4760  csbopeq1a  6359  oaabs2  6847  ecinxp  6938  resixpfo  7059  sbthlem3  7178  rankxpsuc  7762  fseqenlem2  7862  dfac2  7967  isf32lem9  8197  compsscnvlem  8206  ttukeylem7  8351  fpwwe2lem11  8471  00id  9197  submul2  9430  divadddiv  9685  infmsup  9942  xadd4d  10838  fzval3  11135  ceim1l  11189  fldiv  11196  flmod  11217  intfrac  11218  modcyc2  11232  moddi  11239  uzrdgfni  11253  axdc4uzlem  11276  seqf1olem1  11317  seqf1olem2  11318  seqid2  11324  expnegz  11369  binom2sub  11453  binom3  11455  ccatco  11759  swrds2  11835  reim  11869  mulre  11881  addcj  11908  absimle  12069  clim2ser  12403  isercoll2  12417  serf0  12429  iseralt  12433  summolem3  12463  isumclim3  12498  fsumrev  12517  fsumshft  12518  fsum2mul  12527  incexc  12572  isumsplit  12575  mertenslem1  12616  ef4p  12669  tanval3  12690  efival  12708  sinmul  12728  bitsinvp1  12916  sadaddlem  12933  bitsshft  12942  smu01lem  12952  eulerthlem2  13126  pythagtriplem16  13159  pczpre  13176  pcqdiv  13186  pcadd  13213  pcfac  13223  prmreclem5  13243  4sqlem10  13270  4sqlem19  13286  vdwapun  13297  vdwlem1  13304  ramcl  13352  strfvd  13453  strfv2d  13454  xpsff1o  13748  xpslem  13753  2oppccomf  13906  oppcepi  13920  sscfn1  13972  sscfn2  13973  invfuc  14126  grpinvval2  14827  pgp0  15185  sylow1lem1  15187  sylow3lem2  15217  efgredleme  15330  efgcpbllemb  15342  frgpuptinv  15358  frgpup3lem  15364  gexexlem  15422  cyggenod  15449  gsumval3eu  15468  gsumval3  15469  gsumzaddlem  15481  dprd2db  15556  rnginvdv  15754  lss1d  15994  mplcoe3  16484  subrgascl  16513  ply1sclid  16634  znzrh2  16781  ipassr2  16833  ntrval2  17070  ordtuni  17208  cnclima  17286  cmpsub  17417  ptbasfi  17566  txbasval  17591  pt1hmeo  17791  alexsubALTlem1  18031  trust  18212  ussid  18243  ressuss  18246  ressprdsds  18354  imasdsf1olem  18356  setsms  18463  tmsxms  18469  tmsxpsmopn  18520  subgnm  18627  tngnm  18645  tngngp2  18646  xrsxmet  18793  xrge0gsumle  18817  metdstri  18834  xrhmeo  18924  lebnumlem3  18941  pcorevlem  19004  pi1xfrcnvlem  19034  clmabs  19060  minveclem4a  19284  pjthlem1  19291  ovolunlem1a  19345  mbfres2  19490  i1faddlem  19538  ibladdlem  19664  iblabs  19673  ditgsplit  19701  dvnres  19770  dveflem  19816  dveq0  19837  dvfsumabs  19860  itgsubstlem  19885  evlseu  19890  ply1divex  20012  dgrco  20146  plycjlem  20147  taylthlem1  20242  pserdv2  20299  abelthlem6  20305  abelthlem7  20307  tangtx  20366  abssinper  20379  sineq0  20382  explog  20441  reexplog  20442  eflogeq  20449  abslogle  20466  tanarg  20467  logtayl  20504  logtayl2  20506  ang180lem3  20606  affineequiv  20620  affineequiv2  20621  chordthmlem4  20629  chordthmlem5  20630  dcubic1lem  20636  dcubic2  20637  dcubic  20639  mcubic  20640  cubic2  20641  dquartlem1  20644  dquart  20646  quart1lem  20648  quartlem1  20650  quart  20654  acoscos  20686  atanlogaddlem  20706  atantayl2  20731  atantayl3  20732  birthdaylem2  20744  efrlim  20761  amgmlem  20781  logdifbnd  20785  emcllem3  20789  emcllem6  20792  basellem3  20818  basellem8  20823  basellem9  20824  chtprm  20889  logfaclbnd  20959  perfect1  20965  bcp1ctr  21016  bclbnd  21017  bposlem1  21021  lgsdilem  21059  lgsdirnn0  21076  lgsdinn0  21077  lgseisenlem2  21087  lgsquadlem1  21091  2sqlem2  21101  mul2sq  21102  vmadivsum  21129  rpvmasumlem  21134  dchrisumlem1  21136  dchrisumlem2  21137  dchrmusum2  21141  dchrvmasum2if  21144  dchrisum0lem2  21165  logsqvma2  21190  selberg3  21206  selberg4lem1  21207  pntrsumo1  21212  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntibndlem2  21238  pntlemk  21253  pntlemo  21254  ostth2lem4  21283  ostth3  21285  grpoidinvlem2  21746  gxid  21814  subgores  21845  nvmtri  22113  cnnvm  22127  nvnd  22133  ipidsq  22162  ipnm  22163  ipipcj  22167  blocnilem  22258  ipasslem2  22286  dipsubdir  22302  hvaddsubval  22488  pjhthlem1  22846  pjspansn  23032  pjo  23126  unoplin  23376  adjadj  23392  hmoplin  23398  eigvec1  23418  lnopeqi  23464  nmcexi  23482  lnfnsubi  23502  riesz3i  23518  kbass6  23577  leoprf2  23583  leoprf  23584  pjnmopi  23604  mdslmd1lem1  23781  mdslmd1lem2  23782  superpos  23810  xrge0tsmseq  24178  subrgchr  24183  rhmdvd  24212  pstmval  24243  mndpluscn  24265  qqhucn  24329  esumval  24394  gsumesum  24404  esumcst  24408  esumpcvgval  24421  probdif  24631  ballotlemfp1  24702  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  gamigam  24790  lgamcvg2  24792  gamfac  24804  derangen2  24813  subfaclefac  24815  subfaclim  24827  sinccvglem  25062  fprodshft  25253  fprodrev  25254  iprodclim3  25266  brbtwn2  25748  colinearalglem4  25752  axsegconlem1  25760  axpaschlem  25783  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  ltflcei  26140  mblfinlem3  26145  ibladdnclem  26160  iblabsnc  26168  iblmulc2nc  26169  filnetlem4  26300  sdclem2  26336  ismtycnv  26401  heiborlem10  26419  mzpsubmpt  26690  irrapxlem3  26777  pellexlem6  26787  pell1234qrne0  26806  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell14qrdich  26822  pell1qrgaplem  26826  rmxluc  26889  rmyluc  26890  jm2.24nn  26914  jm2.18  26949  jm2.19lem2  26951  jm2.19lem3  26952  jm2.22  26956  jm2.23  26957  jm2.16nn0  26965  jm2.27c  26968  fnwe2lem2  27016  lmhmfgsplit  27052  pwssplit1  27056  dsmmfi  27072  frlmlss  27087  frlmlbs  27117  frlmup3  27120  islindf4  27176  hbtlem2  27196  psgnunilem1  27284  psgnuni  27290  hashgcdeq  27385  dvconstbi  27419  stoweidlem22  27638  stoweidlem32  27648  wallispilem5  27685  stirlinglem5  27694  sigarcol  27721  swrdccatin12lem3  28024  swrdccatin12  28026  swrdccat3b  28031  frg2woteq  28163  recsec  28213  reccsc  28214  bnj1415  29113  lflvsass  29564  lkrscss  29581  eqlkr  29582  eqlkr3  29584  ldualvsdi2  29627  omllaw3  29728  cmtcomlemN  29731  cmtbr3N  29737  omlfh3N  29742  llnexchb2lem  30350  dalawlem7  30359  dalawlem11  30363  dalawlem12  30364  pol1N  30392  paddatclN  30431  4atexlemcnd  30554  ltrncoidN  30610  cdleme3b  30711  cdleme11  30752  cdleme15a  30756  cdleme22e  30826  cdleme22g  30830  cdlemg18b  31161  trlcoat  31205  cdlemk2  31314  cdlemk4  31316  cdlemki  31323  cdlemksv2  31329  cdlemk15  31337  cdlemk55a  31441  diainN  31540  dia2dimlem3  31549  dia2dimlem5  31551  dvhlveclem  31591  diaocN  31608  cdlemn4  31681  cdlemn8  31687  dihopelvalcpre  31731  dihmeetlem9N  31798  dih1dimatlem  31812  dihpN  31819  dochvalr3  31846  dochsat  31866  djhjlj  31886  dochdmm1  31893  dihjatcclem4  31904  dihjat1  31912  dihjat4  31916  dochsnkr2cl  31957  dochfl1  31959  lclkrlem2j  31999  mapdordlem2  32120  mapdrvallem2  32128  hdmap10  32326

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397