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  4654  elxp4  5275  elxp5  5276  funopsn  5891  csbopeq1a  6422  ecinxp  6884  fundmen  7094  fidifsnen  7172  sbthlemi3  7276  ctm  7449  addpinq1  7831  1idsr  8135  prsradd  8153  cnegexlem3  8503  cnegex  8504  submul2  8726  mulsubfacd  8746  divadddivap  9057  infrenegsupex  9994  xadd4d  10287  fzval3  10622  fzoshftral  10657  ceiqm1l  10748  flqdiv  10758  flqmod  10775  intqfrac  10776  modqcyc2  10797  modqdi  10829  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  seqf1oglem1  10956  seqf1oglem2  10957  seq3id2  10963  expnegzap  11010  binom2sub  11090  binom3  11094  resq01  11095  fihashssdif  11259  ccatw2s1p2  11414  ccats1pfxeq  11486  pfxccatin12lem2  11503  pfxccatin12  11505  swrdccat3b  11512  cats1fvnd  11537  reim  11617  mulreap  11629  addcj  11656  resqrexlemcalc1  11780  absimle  11850  infxrnegsupex  12029  clim2ser  12103  serf0  12118  summodclem3  12147  mptfzshft  12209  fsumrev  12210  fsum2mul  12220  isumsplit  12258  cvgratz  12299  mertenslemi1  12302  fprodrev  12386  ef4p  12461  tanval3ap  12481  efival  12499  sinmul  12511  divalglemnn  12685  dfgcd2  12791  lcmgcdlem  12855  lcm1  12859  oddpwdclemxy  12947  oddpwdclemdc  12951  eulerthlemth  13010  hashgcdeq  13018  powm2modprm  13031  pythagtriplem16  13058  pczpre  13076  pcqdiv  13086  pcadd  13119  pcfac  13129  4sqlem10  13166  4sqlem19  13188  ennnfonelemp1  13297  strslfvd  13394  xpsff1o  13670  gzsumsplit1r  13715  grpinvssd  13882  grpinvval2  13888  gzsumreidx  14141  gzsumshift  14149  gzsumgsum1  14153  gzsumgsum  14155  opprrngbg  14383  opprringbg  14385  ringinvdv  14452  lss1d  14720  znzrh2  14981  cnclima  15324  divcncfap  15715  dveflem  15827  plycjlemc  15861  tangtx  15939  abssinper  15947  reexplog  15972  rprelogbdiv  16059  birthdaylem2  16088  perfect1  16112  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1a  16177  gausslemma2dlem4  16183  gausslemma2dlem5a  16184  lgseisenlem2  16190  lgsquadlem1  16196  2sqlem2  16234  mul2sq  16235  ushgredgedgloop  16469  clwwlkext2edg  16663  pw1map  17025