Theorem eqtr4id 2290

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  iftrue  3645  iffalse  3648  difprsn1  3854  dmmptg  5285  relcoi1  5319  funimacnv  5457  dmmptd  5514  dffv3g  5691  dfimafn  5751  fvco2  5774  dfimafnf  5955  isoini  6024  iotaexel  6043  fvmpopr2d  6225  oprabco  6453  suppcofn  6506  ixpconstg  6989  unfiexmid  7225  undifdc  7231  sbthlemi4  7277  sbthlemi5  7278  sbthlemi6  7279  supval2ti  7335  exmidfodomrlemim  7553  suplocexprlemex  8089  eqneg  9064  zeo  9755  fseq1p1m1  10511  seq3val  10910  seqvalcd  10911  hashfzo  11277  hashxp  11281  hashfibclem  11296  wrdval  11321  wrdnval  11349  swrdccat3blem  11525  fsumconst  12237  modfsummod  12241  telfsumo  12249  fprodconst  12403  mulgcd  12809  algcvg  12842  phiprmpw  13020  phisum  13039  strslfv3  13447  resseqnbasd  13476  imasplusg  13678  imasmulr  13679  ismgmid  13746  gzsumshift  14198  pwssnf1o  14260  pws0g  14262  dfrhm2  14510  subrg1  14588  2idlbas  14901  rnascl  15083  psrbagfi  15108  psrlinv  15124  mplbascoe  15131  mplplusgg  15143  uptx  15424  resubmet  15706  ply1termlem  15892  birthdaylem1g  16144  birthdaylem2  16145  lgsval4lem  16228  lgsquadlem2  16295  m1lgs  16302  uspgrf1oedg  16515