Theorem eqtr4id 2283

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  iftrue  3610  iffalse  3613  difprsn1  3812  dmmptg  5234  relcoi1  5268  funimacnv  5406  dmmptd  5463  dffv3g  5635  dfimafn  5694  fvco2  5715  isoini  5959  iotaexel  5976  fvmpopr2d  6158  oprabco  6382  ixpconstg  6876  unfiexmid  7110  undifdc  7116  sbthlemi4  7159  sbthlemi5  7160  sbthlemi6  7161  supval2ti  7194  exmidfodomrlemim  7412  suplocexprlemex  7942  eqneg  8912  zeo  9585  fseq1p1m1  10329  seq3val  10723  seqvalcd  10724  hashfzo  11087  hashxp  11091  wrdval  11120  wrdnval  11148  swrdccat3blem  11324  fsumconst  12033  modfsummod  12037  telfsumo  12045  fprodconst  12199  mulgcd  12605  algcvg  12638  phiprmpw  12812  phisum  12831  strslfv3  13146  resseqnbasd  13174  pwssnf1o  13399  imasplusg  13409  imasmulr  13410  ismgmid  13478  pws0g  13552  dfrhm2  14187  subrg1  14264  2idlbas  14548  psrbagfi  14706  psrlinv  14717  mplbascoe  14724  mplplusgg  14736  uptx  15017  resubmet  15299  ply1termlem  15485  lgsval4lem  15759  lgsquadlem2  15826  m1lgs  15833  uspgrf1oedg  16046  gsumgfsumlem  16735