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  5288  relcoi1  5322  funimacnv  5460  dmmptd  5517  dffv3g  5694  dfimafn  5754  fvco2  5777  dfimafnf  5958  isoini  6027  iotaexel  6046  fvmpopr2d  6228  oprabco  6457  suppcofn  6510  ixpconstg  6993  unfiexmid  7229  undifdc  7235  sbthlemi4  7282  sbthlemi5  7283  sbthlemi6  7284  supval2ti  7341  exmidfodomrlemim  7559  suplocexprlemex  8095  eqneg  9070  zeo  9762  fseq1p1m1  10518  seq3val  10918  seqvalcd  10919  hashfzo  11285  hashxp  11289  hashfibclem  11304  wrdval  11329  wrdnval  11357  swrdccat3blem  11533  fsumconst  12246  modfsummod  12250  telfsumo  12258  fprodconst  12412  mulgcd  12818  algcvg  12851  phiprmpw  13029  phisum  13048  strslfv3  13456  resseqnbasd  13486  imasplusg  13688  imasmulr  13689  ismgmid  13756  gzsumshift  14239  pwssnf1o  14318  pws0g  14320  dfrhm2  14570  subrg1  14648  2idlbas  14961  rnascl  15143  psrbagfi  15168  psrlinv  15194  mplbascoe  15207  mplplusgg  15219  uptx  15500  resubmet  15782  ply1termlem  15968  birthdaylem1g  16225  birthdaylem2  16226  chtqub  16296  lgsval4lem  16335  lgsquadlem2  16402  m1lgs  16409  uspgrf1oedg  16622