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 )

Syntax hints:   -> wi 4   = wceq 1402

This theorem was proved from 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 theorem depends on definitions:  df-bi 117  df-cleq 2231

This theorem is referenced by:  3eqtrrd  2276  3eqtr2rd  2278  ifandc  3678  ifordc  3679  onsucmin  4649  elxp4  5270  elxp5  5271  funopsn  5882  csbopeq1a  6412  ecinxp  6874  fundmen  7084  fidifsnen  7162  sbthlemi3  7266  ctm  7439  addpinq1  7821  1idsr  8125  prsradd  8143  cnegexlem3  8493  cnegex  8494  submul2  8716  mulsubfacd  8736  divadddivap  9047  infrenegsupex  9973  xadd4d  10266  fzval3  10600  fzoshftral  10635  ceiqm1l  10726  flqdiv  10736  flqmod  10753  intqfrac  10754  modqcyc2  10775  modqdi  10807  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  seqf1oglem1  10934  seqf1oglem2  10935  seq3id2  10941  expnegzap  10988  binom2sub  11068  binom3  11072  resq01  11073  fihashssdif  11237  ccatw2s1p2  11392  ccats1pfxeq  11464  pfxccatin12lem2  11481  pfxccatin12  11483  swrdccat3b  11490  cats1fvnd  11515  reim  11595  mulreap  11607  addcj  11634  resqrexlemcalc1  11758  absimle  11828  infxrnegsupex  12007  clim2ser  12081  serf0  12096  summodclem3  12125  mptfzshft  12187  fsumrev  12188  fsum2mul  12198  isumsplit  12236  cvgratz  12277  mertenslemi1  12280  fprodrev  12364  ef4p  12439  tanval3ap  12459  efival  12477  sinmul  12489  divalglemnn  12663  dfgcd2  12769  lcmgcdlem  12833  lcm1  12837  oddpwdclemxy  12925  oddpwdclemdc  12929  eulerthlemth  12988  hashgcdeq  12996  powm2modprm  13009  pythagtriplem16  13036  pczpre  13054  pcqdiv  13064  pcadd  13097  pcfac  13107  4sqlem10  13144  4sqlem19  13166  ennnfonelemp1  13275  strslfvd  13372  xpsff1o  13647  gzsumsplit1r  13692  grpinvssd  13859  grpinvval2  13865  gzsumreidx  14118  gzsumshift  14126  gzsumgsum1  14130  gzsumgsum  14132  opprrngbg  14356  opprringbg  14358  ringinvdv  14425  lss1d  14692  znzrh2  14953  cnclima  15247  divcncfap  15638  dveflem  15750  plycjlemc  15784  tangtx  15862  abssinper  15870  reexplog  15895  rprelogbdiv  15982  perfect1  16026  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1a  16091  gausslemma2dlem4  16097  gausslemma2dlem5a  16098  lgseisenlem2  16104  lgsquadlem1  16110  2sqlem2  16148  mul2sq  16149  ushgredgedgloop  16383  clwwlkext2edg  16577  pw1map  16939