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  5179  relcoi1  5213  funimacnv  5349  dmmptd  5405  dffv3g  5571  dfimafn  5626  fvco2  5647  isoini  5886  iotaexel  5903  fvmpopr2d  6081  oprabco  6302  ixpconstg  6793  unfiexmid  7014  undifdc  7020  sbthlemi4  7061  sbthlemi5  7062  sbthlemi6  7063  supval2ti  7096  exmidfodomrlemim  7308  suplocexprlemex  7834  eqneg  8804  zeo  9477  fseq1p1m1  10215  seq3val  10603  seqvalcd  10604  hashfzo  10965  hashxp  10969  wrdval  10995  wrdnval  11022  fsumconst  11736  modfsummod  11740  telfsumo  11748  fprodconst  11902  mulgcd  12308  algcvg  12341  phiprmpw  12515  phisum  12534  strslfv3  12849  resseqnbasd  12876  pwssnf1o  13101  imasplusg  13111  imasmulr  13112  ismgmid  13180  pws0g  13254  dfrhm2  13887  subrg1  13964  2idlbas  14248  psrbagfi  14406  psrlinv  14417  mplbascoe  14424  mplplusgg  14436  uptx  14717  resubmet  14999  ply1termlem  15185  lgsval4lem  15459  lgsquadlem2  15526  m1lgs  15533