Theorem eqtr2d 2241

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  3eqtrrd  2245  3eqtr2rd  2247  ifandc  3620  ifordc  3621  onsucmin  4573  elxp4  5189  elxp5  5190  funopsn  5785  csbopeq1a  6297  ecinxp  6720  fundmen  6922  fidifsnen  6993  sbthlemi3  7087  ctm  7237  addpinq1  7612  1idsr  7916  prsradd  7934  cnegexlem3  8284  cnegex  8285  submul2  8506  mulsubfacd  8526  divadddivap  8835  infrenegsupex  9750  xadd4d  10042  fzval3  10370  fzoshftral  10404  ceiqm1l  10493  flqdiv  10503  flqmod  10520  intqfrac  10521  modqcyc2  10542  modqdi  10574  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  seqf1oglem1  10701  seqf1oglem2  10702  seq3id2  10708  expnegzap  10755  binom2sub  10835  binom3  10839  fihashssdif  11000  ccatw2s1p2  11135  ccats1pfxeq  11205  pfxccatin12lem2  11222  pfxccatin12  11224  swrdccat3b  11231  reim  11278  mulreap  11290  addcj  11317  resqrexlemcalc1  11440  absimle  11510  infxrnegsupex  11689  clim2ser  11763  serf0  11778  summodclem3  11806  mptfzshft  11868  fsumrev  11869  fsum2mul  11879  isumsplit  11917  cvgratz  11958  mertenslemi1  11961  fprodrev  12045  ef4p  12120  tanval3ap  12140  efival  12158  sinmul  12170  divalglemnn  12344  dfgcd2  12450  lcmgcdlem  12514  lcm1  12518  oddpwdclemxy  12606  oddpwdclemdc  12610  eulerthlemth  12669  hashgcdeq  12677  powm2modprm  12690  pythagtriplem16  12717  pczpre  12735  pcqdiv  12745  pcadd  12778  pcfac  12788  4sqlem10  12825  4sqlem19  12847  ennnfonelemp1  12892  strslfvd  12989  xpsff1o  13296  gsumsplit1r  13345  grpinvssd  13524  grpinvval2  13530  gsumfzreidx  13788  opprrngbg  13955  opprringbg  13957  ringinvdv  14022  lss1d  14260  znzrh2  14523  cnclima  14810  divcncfap  15201  dveflem  15313  plycjlemc  15347  tangtx  15425  abssinper  15433  reexplog  15458  rprelogbdiv  15544  perfect1  15585  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1a  15650  gausslemma2dlem4  15656  gausslemma2dlem5a  15657  lgseisenlem2  15663  lgsquadlem1  15669  2sqlem2  15707  mul2sq  15708  pw1map  16134