Theorem eqtr4id 2256

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

Syntax hints:   -> wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  iftrue  3575  iffalse  3578  difprsn1  3771  dmmptg  5177  relcoi1  5211  funimacnv  5344  dmmptd  5400  dffv3g  5566  dfimafn  5621  fvco2  5642  isoini  5877  iotaexel  5894  fvmpopr2d  6072  oprabco  6293  ixpconstg  6784  unfiexmid  6997  undifdc  7003  sbthlemi4  7044  sbthlemi5  7045  sbthlemi6  7046  supval2ti  7079  exmidfodomrlemim  7291  suplocexprlemex  7817  eqneg  8787  zeo  9460  fseq1p1m1  10198  seq3val  10586  seqvalcd  10587  hashfzo  10948  hashxp  10952  wrdval  10972  wrdnval  10999  fsumconst  11684  modfsummod  11688  telfsumo  11696  fprodconst  11850  mulgcd  12256  algcvg  12289  phiprmpw  12463  phisum  12482  strslfv3  12797  resseqnbasd  12824  pwssnf1o  13048  imasplusg  13058  imasmulr  13059  ismgmid  13127  pws0g  13201  dfrhm2  13834  subrg1  13911  2idlbas  14195  psrbagfi  14353  psrlinv  14364  mplbascoe  14371  mplplusgg  14383  uptx  14664  resubmet  14946  ply1termlem  15132  lgsval4lem  15406  lgsquadlem2  15473  m1lgs  15480