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  11707  modfsummod  11711  telfsumo  11719  fprodconst  11873  mulgcd  12279  algcvg  12312  phiprmpw  12486  phisum  12505  strslfv3  12820  resseqnbasd  12847  pwssnf1o  13072  imasplusg  13082  imasmulr  13083  ismgmid  13151  pws0g  13225  dfrhm2  13858  subrg1  13935  2idlbas  14219  psrbagfi  14377  psrlinv  14388  mplbascoe  14395  mplplusgg  14407  uptx  14688  resubmet  14970  ply1termlem  15156  lgsval4lem  15430  lgsquadlem2  15497  m1lgs  15504