Theorem eqtr4id 2258

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  iftrue  3580  iffalse  3583  difprsn1  3778  dmmptg  5189  relcoi1  5223  funimacnv  5359  dmmptd  5416  dffv3g  5585  dfimafn  5640  fvco2  5661  isoini  5900  iotaexel  5917  fvmpopr2d  6095  oprabco  6316  ixpconstg  6807  unfiexmid  7030  undifdc  7036  sbthlemi4  7077  sbthlemi5  7078  sbthlemi6  7079  supval2ti  7112  exmidfodomrlemim  7325  suplocexprlemex  7855  eqneg  8825  zeo  9498  fseq1p1m1  10236  seq3val  10627  seqvalcd  10628  hashfzo  10989  hashxp  10993  wrdval  11019  wrdnval  11046  fsumconst  11840  modfsummod  11844  telfsumo  11852  fprodconst  12006  mulgcd  12412  algcvg  12445  phiprmpw  12619  phisum  12638  strslfv3  12953  resseqnbasd  12980  pwssnf1o  13205  imasplusg  13215  imasmulr  13216  ismgmid  13284  pws0g  13358  dfrhm2  13991  subrg1  14068  2idlbas  14352  psrbagfi  14510  psrlinv  14521  mplbascoe  14528  mplplusgg  14540  uptx  14821  resubmet  15103  ply1termlem  15289  lgsval4lem  15563  lgsquadlem2  15630  m1lgs  15637