Theorem eqtr4id 2206

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

Syntax hints:   -> wi 4   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-cleq 2147

This theorem is referenced by:  iftrue  3506  iffalse  3509  difprsn1  3691  dmmptg  5076  relcoi1  5110  funimacnv  5239  dmmptd  5293  dffv3g  5457  dfimafn  5510  fvco2  5530  isoini  5759  oprabco  6154  ixpconstg  6641  unfiexmid  6851  undifdc  6857  sbthlemi4  6893  sbthlemi5  6894  sbthlemi6  6895  supval2ti  6927  exmidfodomrlemim  7115  suplocexprlemex  7621  eqneg  8584  zeo  9248  fseq1p1m1  9974  seq3val  10335  seqvalcd  10336  hashfzo  10673  hashxp  10677  fsumconst  11328  modfsummod  11332  telfsumo  11340  fprodconst  11494  mulgcd  11871  algcvg  11896  phiprmpw  12065  strslfv3  12174  uptx  12613  resubmet  12887