Theorem eqtr4id 2281

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  iftrue  3607  iffalse  3610  difprsn1  3806  dmmptg  5225  relcoi1  5259  funimacnv  5396  dmmptd  5453  dffv3g  5622  dfimafn  5681  fvco2  5702  isoini  5941  iotaexel  5958  fvmpopr2d  6140  oprabco  6361  ixpconstg  6852  unfiexmid  7076  undifdc  7082  sbthlemi4  7123  sbthlemi5  7124  sbthlemi6  7125  supval2ti  7158  exmidfodomrlemim  7375  suplocexprlemex  7905  eqneg  8875  zeo  9548  fseq1p1m1  10286  seq3val  10677  seqvalcd  10678  hashfzo  11039  hashxp  11043  wrdval  11069  wrdnval  11097  swrdccat3blem  11266  fsumconst  11960  modfsummod  11964  telfsumo  11972  fprodconst  12126  mulgcd  12532  algcvg  12565  phiprmpw  12739  phisum  12758  strslfv3  13073  resseqnbasd  13101  pwssnf1o  13326  imasplusg  13336  imasmulr  13337  ismgmid  13405  pws0g  13479  dfrhm2  14112  subrg1  14189  2idlbas  14473  psrbagfi  14631  psrlinv  14642  mplbascoe  14649  mplplusgg  14661  uptx  14942  resubmet  15224  ply1termlem  15410  lgsval4lem  15684  lgsquadlem2  15751  m1lgs  15758  uspgrf1oedg  15968