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  9062  zeo  9751  fseq1p1m1  10501  seq3val  10897  seqvalcd  10898  hashfzo  11263  hashxp  11267  hashfibclem  11282  wrdval  11307  wrdnval  11335  swrdccat3blem  11511  fsumconst  12221  modfsummod  12225  telfsumo  12233  fprodconst  12387  mulgcd  12793  algcvg  12826  phiprmpw  13000  phisum  13019  strslfv3  13398  resseqnbasd  13427  imasplusg  13629  imasmulr  13630  ismgmid  13697  gzsumshift  14149  pwssnf1o  14211  pws0g  14213  dfrhm2  14461  subrg1  14539  2idlbas  14852  rnascl  15034  psrbagfi  15059  psrlinv  15075  mplbascoe  15082  mplplusgg  15094  uptx  15375  resubmet  15657  ply1termlem  15843  birthdaylem1g  16087  birthdaylem2  16088  lgsval4lem  16130  lgsquadlem2  16197  m1lgs  16204  uspgrf1oedg  16417