Theorem eqtr2d 2272

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtrrd  2276  3eqtr2rd  2278  ifandc  3681  ifordc  3682  onsucmin  4656  elxp4  5278  elxp5  5279  funopsn  5894  csbopeq1a  6426  ecinxp  6888  fundmen  7098  fidifsnen  7176  sbthlemi3  7281  ctm  7455  addpinq1  7837  1idsr  8141  prsradd  8159  cnegexlem3  8510  cnegex  8511  submul2  8733  mulsubfacd  8753  divadddivap  9065  infrenegsupex  10010  xadd4d  10304  fzval3  10639  fzoshftral  10674  ceiqm1l  10769  flqdiv  10779  flqmod  10796  intqfrac  10797  modqcyc2  10818  modqdi  10850  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seqf1oglem1  10977  seqf1oglem2  10978  seq3id2  10984  expnegzap  11031  binom2sub  11111  binom3  11115  resq01  11116  fihashssdif  11281  ccatw2s1p2  11436  ccats1pfxeq  11508  pfxccatin12lem2  11525  pfxccatin12  11527  swrdccat3b  11534  cats1fvnd  11559  reim  11639  mulreap  11651  addcj  11678  resqrexlemcalc1  11802  absimle  11873  infxrnegsupex  12054  clim2ser  12128  serf0  12143  summodclem3  12172  mptfzshft  12234  fsumrev  12235  fsum2mul  12245  isumsplit  12283  cvgratz  12324  mertenslemi1  12327  fprodrev  12411  ef4p  12486  tanval3ap  12506  efival  12524  sinmul  12536  divalglemnn  12710  dfgcd2  12816  lcmgcdlem  12880  lcm1  12884  nnmaxpwlemxy  12973  nnmaxpwlemparts  12977  eulerthlemth  13039  hashgcdeq  13047  powm2modprm  13060  pythagtriplem16  13087  pczpre  13105  pcqdiv  13115  pcadd  13148  pcfac  13158  4sqlem10  13195  4sqlem19  13217  ennnfonelemp1  13355  strslfvd  13452  xpsff1o  13729  gzsumsplit1r  13774  grpinvssd  13941  grpinvval2  13947  gzsumreidx  14231  gzsumshift  14239  gzsumgsum1  14243  gzsumgsum  14245  opprrngbg  14492  opprringbg  14494  ringinvdv  14561  lss1d  14829  znzrh2  15090  cnclima  15449  divcncfap  15840  dveflem  15952  plycjlemc  15986  tangtx  16065  abssinper  16073  sineq0re  16076  reexplog  16101  rprelogbdiv  16193  birthdaylem2  16226  chtprm  16261  perfect1  16298  bcp1ctr  16306  bclbnd  16307  bposlem1  16311  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1a  16382  gausslemma2dlem4  16388  gausslemma2dlem5a  16389  lgseisenlem2  16395  lgsquadlem1  16401  2sqlem2  16439  mul2sq  16440  ushgredgedgloop  16674  clwwlkext2edg  16868  pw1map  17230