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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  iftrue  3610  iffalse  3613  difprsn1  3812  dmmptg  5234  relcoi1  5268  funimacnv  5406  dmmptd  5463  dffv3g  5635  dfimafn  5694  fvco2  5715  isoini  5958  iotaexel  5975  fvmpopr2d  6157  oprabco  6381  ixpconstg  6875  unfiexmid  7109  undifdc  7115  sbthlemi4  7158  sbthlemi5  7159  sbthlemi6  7160  supval2ti  7193  exmidfodomrlemim  7411  suplocexprlemex  7941  eqneg  8911  zeo  9584  fseq1p1m1  10328  seq3val  10721  seqvalcd  10722  hashfzo  11085  hashxp  11089  wrdval  11115  wrdnval  11143  swrdccat3blem  11319  fsumconst  12014  modfsummod  12018  telfsumo  12026  fprodconst  12180  mulgcd  12586  algcvg  12619  phiprmpw  12793  phisum  12812  strslfv3  13127  resseqnbasd  13155  pwssnf1o  13380  imasplusg  13390  imasmulr  13391  ismgmid  13459  pws0g  13533  dfrhm2  14167  subrg1  14244  2idlbas  14528  psrbagfi  14686  psrlinv  14697  mplbascoe  14704  mplplusgg  14716  uptx  14997  resubmet  15279  ply1termlem  15465  lgsval4lem  15739  lgsquadlem2  15806  m1lgs  15813  uspgrf1oedg  16026  gsumgfsumlem  16683