Theorem eqtr4id 2229

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  iftrue  3540  iffalse  3543  difprsn1  3732  dmmptg  5127  relcoi1  5161  funimacnv  5293  dmmptd  5347  dffv3g  5512  dfimafn  5565  fvco2  5586  isoini  5819  oprabco  6218  ixpconstg  6707  unfiexmid  6917  undifdc  6923  sbthlemi4  6959  sbthlemi5  6960  sbthlemi6  6961  supval2ti  6994  exmidfodomrlemim  7200  suplocexprlemex  7721  eqneg  8689  zeo  9358  fseq1p1m1  10094  seq3val  10458  seqvalcd  10459  hashfzo  10802  hashxp  10806  fsumconst  11462  modfsummod  11466  telfsumo  11474  fprodconst  11628  mulgcd  12017  algcvg  12048  phiprmpw  12222  phisum  12240  strslfv3  12508  resseqnbasd  12532  imasplusg  12729  imasmulr  12730  ismgmid  12796  subrg1  13352  uptx  13777  resubmet  14051  lgsval4lem  14415  m1lgs  14455