Theorem eqtr2d 2263

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtrrd  2267  3eqtr2rd  2269  ifandc  3644  ifordc  3645  onsucmin  4603  elxp4  5222  elxp5  5223  funopsn  5825  csbopeq1a  6346  ecinxp  6774  fundmen  6976  fidifsnen  7052  sbthlemi3  7149  ctm  7299  addpinq1  7674  1idsr  7978  prsradd  7996  cnegexlem3  8346  cnegex  8347  submul2  8568  mulsubfacd  8588  divadddivap  8897  infrenegsupex  9818  xadd4d  10110  fzval3  10439  fzoshftral  10474  ceiqm1l  10563  flqdiv  10573  flqmod  10590  intqfrac  10591  modqcyc2  10612  modqdi  10644  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  seqf1oglem1  10771  seqf1oglem2  10772  seq3id2  10778  expnegzap  10825  binom2sub  10905  binom3  10909  fihashssdif  11072  ccatw2s1p2  11213  ccats1pfxeq  11285  pfxccatin12lem2  11302  pfxccatin12  11304  swrdccat3b  11311  cats1fvnd  11336  reim  11403  mulreap  11415  addcj  11442  resqrexlemcalc1  11565  absimle  11635  infxrnegsupex  11814  clim2ser  11888  serf0  11903  summodclem3  11931  mptfzshft  11993  fsumrev  11994  fsum2mul  12004  isumsplit  12042  cvgratz  12083  mertenslemi1  12086  fprodrev  12170  ef4p  12245  tanval3ap  12265  efival  12283  sinmul  12295  divalglemnn  12469  dfgcd2  12575  lcmgcdlem  12639  lcm1  12643  oddpwdclemxy  12731  oddpwdclemdc  12735  eulerthlemth  12794  hashgcdeq  12802  powm2modprm  12815  pythagtriplem16  12842  pczpre  12860  pcqdiv  12870  pcadd  12903  pcfac  12913  4sqlem10  12950  4sqlem19  12972  ennnfonelemp1  13017  strslfvd  13114  xpsff1o  13422  gsumsplit1r  13471  grpinvssd  13650  grpinvval2  13656  gsumfzreidx  13914  opprrngbg  14081  opprringbg  14083  ringinvdv  14149  lss1d  14387  znzrh2  14650  cnclima  14937  divcncfap  15328  dveflem  15440  plycjlemc  15474  tangtx  15552  abssinper  15560  reexplog  15585  rprelogbdiv  15671  perfect1  15712  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1a  15777  gausslemma2dlem4  15783  gausslemma2dlem5a  15784  lgseisenlem2  15790  lgsquadlem1  15796  2sqlem2  15834  mul2sq  15835  ushgredgedgloop  16067  clwwlkext2edg  16217  pw1map  16532