Theorem eqtr4id 2284

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  iftrue  3627  iffalse  3630  difprsn1  3833  dmmptg  5260  relcoi1  5294  funimacnv  5432  dmmptd  5489  dffv3g  5666  dfimafn  5725  fvco2  5746  isoini  5991  iotaexel  6008  fvmpopr2d  6190  oprabco  6413  suppcofn  6466  ixpconstg  6942  unfiexmid  7178  undifdc  7184  sbthlemi4  7230  sbthlemi5  7231  sbthlemi6  7232  supval2ti  7286  exmidfodomrlemim  7504  suplocexprlemex  8037  eqneg  9006  zeo  9683  fseq1p1m1  10428  seq3val  10822  seqvalcd  10823  hashfzo  11187  hashxp  11191  hashfibclem  11206  wrdval  11227  wrdnval  11255  swrdccat3blem  11431  fsumconst  12140  modfsummod  12144  telfsumo  12152  fprodconst  12306  mulgcd  12712  algcvg  12745  phiprmpw  12919  phisum  12938  strslfv3  13258  resseqnbasd  13286  pwssnf1o  13511  imasplusg  13521  imasmulr  13522  ismgmid  13590  pws0g  13664  dfrhm2  14299  subrg1  14376  2idlbas  14663  psrbagfi  14823  psrlinv  14839  mplbascoe  14846  mplplusgg  14858  uptx  15139  resubmet  15421  ply1termlem  15607  lgsval4lem  15884  lgsquadlem2  15951  m1lgs  15958  uspgrf1oedg  16171  gsumgfsumlem  16865