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  3539  iffalse  3542  difprsn1  3731  dmmptg  5126  relcoi1  5160  funimacnv  5292  dmmptd  5346  dffv3g  5511  dfimafn  5564  fvco2  5585  isoini  5818  oprabco  6217  ixpconstg  6706  unfiexmid  6916  undifdc  6922  sbthlemi4  6958  sbthlemi5  6959  sbthlemi6  6960  supval2ti  6993  exmidfodomrlemim  7199  suplocexprlemex  7720  eqneg  8688  zeo  9357  fseq1p1m1  10093  seq3val  10457  seqvalcd  10458  hashfzo  10801  hashxp  10805  fsumconst  11461  modfsummod  11465  telfsumo  11473  fprodconst  11627  mulgcd  12016  algcvg  12047  phiprmpw  12221  phisum  12239  strslfv3  12507  resseqnbasd  12531  imasplusg  12728  imasmulr  12729  ismgmid  12795  subrg1  13350  uptx  13744  resubmet  14018  lgsval4lem  14382  m1lgs  14422