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  6889  fundmen  7100  fidifsnen  7178  sbthlemi3  7283  ctm  7455  addpinq1  7837  1idsr  8141  prsradd  8159  cnegexlem3  8510  cnegex  8511  submul2  8733  mulsubfacd  8753  divadddivap  9065  infrenegsupex  10009  xadd4d  10303  fzval3  10638  fzoshftral  10673  ceiqm1l  10768  flqdiv  10778  flqmod  10795  intqfrac  10796  modqcyc2  10817  modqdi  10849  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  seqf1oglem1  10976  seqf1oglem2  10977  seq3id2  10983  expnegzap  11030  binom2sub  11110  binom3  11114  resq01  11115  fihashssdif  11280  ccatw2s1p2  11435  ccats1pfxeq  11507  pfxccatin12lem2  11524  pfxccatin12  11526  swrdccat3b  11533  cats1fvnd  11558  reim  11638  mulreap  11650  addcj  11677  resqrexlemcalc1  11801  absimle  11872  infxrnegsupex  12053  clim2ser  12127  serf0  12142  summodclem3  12171  mptfzshft  12233  fsumrev  12234  fsum2mul  12244  isumsplit  12282  cvgratz  12323  mertenslemi1  12326  fprodrev  12410  ef4p  12485  tanval3ap  12505  efival  12523  sinmul  12535  divalglemnn  12709  dfgcd2  12815  lcmgcdlem  12879  lcm1  12883  nnmaxpwlemxy  12972  nnmaxpwlemparts  12976  eulerthlemth  13038  hashgcdeq  13046  powm2modprm  13059  pythagtriplem16  13086  pczpre  13104  pcqdiv  13114  pcadd  13147  pcfac  13157  4sqlem10  13194  4sqlem19  13216  ennnfonelemp1  13354  strslfvd  13451  xpsff1o  13728  gzsumsplit1r  13773  grpinvssd  13940  grpinvval2  13946  gzsumreidx  14230  gzsumshift  14238  gzsumgsum1  14242  gzsumgsum  14244  opprrngbg  14491  opprringbg  14493  ringinvdv  14560  lss1d  14828  znzrh2  15089  cnclima  15466  divcncfap  15857  dveflem  15969  plycjlemc  16003  tangtx  16082  abssinper  16090  sineq0re  16093  reexplog  16118  rprelogbdiv  16210  birthdaylem2  16243  chtprm  16278  perfect1  16315  bcp1ctr  16323  bclbnd  16324  bposlem1  16328  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem4  16405  gausslemma2dlem5a  16406  lgseisenlem2  16412  lgsquadlem1  16418  2sqlem2  16456  mul2sq  16457  ushgredgedgloop  16691  clwwlkext2edg  16885  pw1map  17247