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  7336  exmidfodomrlemim  7554  suplocexprlemex  8090  eqneg  9065  zeo  9756  fseq1p1m1  10512  seq3val  10912  seqvalcd  10913  hashfzo  11279  hashxp  11283  hashfibclem  11298  wrdval  11323  wrdnval  11351  swrdccat3blem  11527  fsumconst  12240  modfsummod  12244  telfsumo  12252  fprodconst  12406  mulgcd  12812  algcvg  12845  phiprmpw  13023  phisum  13042  strslfv3  13450  resseqnbasd  13480  imasplusg  13682  imasmulr  13683  ismgmid  13750  gzsumshift  14233  pwssnf1o  14295  pws0g  14297  dfrhm2  14545  subrg1  14623  2idlbas  14936  rnascl  15118  psrbagfi  15143  psrlinv  15166  mplbascoe  15173  mplplusgg  15185  uptx  15466  resubmet  15748  ply1termlem  15934  birthdaylem1g  16186  birthdaylem2  16187  chtqub  16257  lgsval4lem  16296  lgsquadlem2  16363  m1lgs  16370  uspgrf1oedg  16583