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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  iftrue  3642  iffalse  3645  difprsn1  3849  dmmptg  5280  relcoi1  5314  funimacnv  5452  dmmptd  5509  dffv3g  5686  dfimafn  5745  fvco2  5768  dfimafnf  5945  isoini  6014  iotaexel  6033  fvmpopr2d  6215  oprabco  6443  suppcofn  6496  ixpconstg  6979  unfiexmid  7215  undifdc  7221  sbthlemi4  7267  sbthlemi5  7268  sbthlemi6  7269  supval2ti  7325  exmidfodomrlemim  7543  suplocexprlemex  8079  eqneg  9052  zeo  9730  fseq1p1m1  10479  seq3val  10875  seqvalcd  10876  hashfzo  11241  hashxp  11245  hashfibclem  11260  wrdval  11285  wrdnval  11313  swrdccat3blem  11489  fsumconst  12199  modfsummod  12203  telfsumo  12211  fprodconst  12365  mulgcd  12771  algcvg  12804  phiprmpw  12978  phisum  12997  strslfv3  13376  resseqnbasd  13404  imasplusg  13606  imasmulr  13607  ismgmid  13674  gzsumshift  14126  pwssnf1o  14188  pws0g  14190  dfrhm2  14434  subrg1  14512  2idlbas  14824  psrbagfi  14982  psrlinv  14998  mplbascoe  15005  mplplusgg  15017  uptx  15298  resubmet  15580  ply1termlem  15766  lgsval4lem  16044  lgsquadlem2  16111  m1lgs  16118  uspgrf1oedg  16331