Theorem eqtr2d 2265

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  3eqtrrd  2269  3eqtr2rd  2271  ifandc  3646  ifordc  3647  onsucmin  4605  elxp4  5224  elxp5  5225  funopsn  5829  csbopeq1a  6350  ecinxp  6778  fundmen  6980  fidifsnen  7056  sbthlemi3  7157  ctm  7307  addpinq1  7683  1idsr  7987  prsradd  8005  cnegexlem3  8355  cnegex  8356  submul2  8577  mulsubfacd  8597  divadddivap  8906  infrenegsupex  9827  xadd4d  10119  fzval3  10448  fzoshftral  10483  ceiqm1l  10572  flqdiv  10582  flqmod  10599  intqfrac  10600  modqcyc2  10621  modqdi  10653  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  seqf1oglem1  10780  seqf1oglem2  10781  seq3id2  10787  expnegzap  10834  binom2sub  10914  binom3  10918  fihashssdif  11081  ccatw2s1p2  11222  ccats1pfxeq  11294  pfxccatin12lem2  11311  pfxccatin12  11313  swrdccat3b  11320  cats1fvnd  11345  reim  11412  mulreap  11424  addcj  11451  resqrexlemcalc1  11574  absimle  11644  infxrnegsupex  11823  clim2ser  11897  serf0  11912  summodclem3  11940  mptfzshft  12002  fsumrev  12003  fsum2mul  12013  isumsplit  12051  cvgratz  12092  mertenslemi1  12095  fprodrev  12179  ef4p  12254  tanval3ap  12274  efival  12292  sinmul  12304  divalglemnn  12478  dfgcd2  12584  lcmgcdlem  12648  lcm1  12652  oddpwdclemxy  12740  oddpwdclemdc  12744  eulerthlemth  12803  hashgcdeq  12811  powm2modprm  12824  pythagtriplem16  12851  pczpre  12869  pcqdiv  12879  pcadd  12912  pcfac  12922  4sqlem10  12959  4sqlem19  12981  ennnfonelemp1  13026  strslfvd  13123  xpsff1o  13431  gsumsplit1r  13480  grpinvssd  13659  grpinvval2  13665  gsumfzreidx  13923  opprrngbg  14090  opprringbg  14092  ringinvdv  14158  lss1d  14396  znzrh2  14659  cnclima  14946  divcncfap  15337  dveflem  15449  plycjlemc  15483  tangtx  15561  abssinper  15569  reexplog  15594  rprelogbdiv  15680  perfect1  15721  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1a  15786  gausslemma2dlem4  15792  gausslemma2dlem5a  15793  lgseisenlem2  15799  lgsquadlem1  15805  2sqlem2  15843  mul2sq  15844  ushgredgedgloop  16078  clwwlkext2edg  16272  pw1map  16596  gsumgfsum1  16681  gsumgfsum  16684