Theorem eqtr4id 2283

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr4id.2	|- A = B
eqtr4id.1	|- ( ph -> C = B )

Assertion

Ref	Expression
eqtr4id	|- ( ph -> A = C )

Proof of Theorem eqtr4id

Step	Hyp	Ref	Expression
1		eqtr4id.1	. 2 |- ( ph -> C = B )
2		eqtr4id.2	. . 3 |- A = B
3	2	eqcomi 2235	. 2 |- B = A
4	1, 3	eqtr2di 2281	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  iftrue  3614  iffalse  3617  difprsn1  3817  dmmptg  5241  relcoi1  5275  funimacnv  5413  dmmptd  5470  dffv3g  5644  dfimafn  5703  fvco2  5724  isoini  5969  iotaexel  5986  fvmpopr2d  6168  oprabco  6391  suppcofn  6444  ixpconstg  6919  unfiexmid  7153  undifdc  7159  sbthlemi4  7202  sbthlemi5  7203  sbthlemi6  7204  supval2ti  7237  exmidfodomrlemim  7455  suplocexprlemex  7985  eqneg  8954  zeo  9629  fseq1p1m1  10374  seq3val  10768  seqvalcd  10769  hashfzo  11132  hashxp  11136  wrdval  11165  wrdnval  11193  swrdccat3blem  11369  fsumconst  12078  modfsummod  12082  telfsumo  12090  fprodconst  12244  mulgcd  12650  algcvg  12683  phiprmpw  12857  phisum  12876  strslfv3  13191  resseqnbasd  13219  pwssnf1o  13444  imasplusg  13454  imasmulr  13455  ismgmid  13523  pws0g  13597  dfrhm2  14232  subrg1  14309  2idlbas  14594  psrbagfi  14753  psrlinv  14768  mplbascoe  14775  mplplusgg  14787  uptx  15068  resubmet  15350  ply1termlem  15536  lgsval4lem  15813  lgsquadlem2  15880  m1lgs  15887  uspgrf1oedg  16100  gsumgfsumlem  16795