Theorem eqtr4id 2281

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 2233	. 2 |- B = A
4	1, 3	eqtr2di 2279	1 |- ( ph -> A = C )

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:  iftrue  3608  iffalse  3611  difprsn1  3810  dmmptg  5232  relcoi1  5266  funimacnv  5403  dmmptd  5460  dffv3g  5631  dfimafn  5690  fvco2  5711  isoini  5954  iotaexel  5971  fvmpopr2d  6153  oprabco  6377  ixpconstg  6871  unfiexmid  7103  undifdc  7109  sbthlemi4  7150  sbthlemi5  7151  sbthlemi6  7152  supval2ti  7185  exmidfodomrlemim  7402  suplocexprlemex  7932  eqneg  8902  zeo  9575  fseq1p1m1  10319  seq3val  10712  seqvalcd  10713  hashfzo  11076  hashxp  11080  wrdval  11106  wrdnval  11134  swrdccat3blem  11310  fsumconst  12005  modfsummod  12009  telfsumo  12017  fprodconst  12171  mulgcd  12577  algcvg  12610  phiprmpw  12784  phisum  12803  strslfv3  13118  resseqnbasd  13146  pwssnf1o  13371  imasplusg  13381  imasmulr  13382  ismgmid  13450  pws0g  13524  dfrhm2  14158  subrg1  14235  2idlbas  14519  psrbagfi  14677  psrlinv  14688  mplbascoe  14695  mplplusgg  14707  uptx  14988  resubmet  15270  ply1termlem  15456  lgsval4lem  15730  lgsquadlem2  15797  m1lgs  15804  uspgrf1oedg  16015