Theorem eqtr4id 2222

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

Syntax hints:   -> wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  iftrue  3530  iffalse  3533  difprsn1  3717  dmmptg  5106  relcoi1  5140  funimacnv  5272  dmmptd  5326  dffv3g  5490  dfimafn  5543  fvco2  5563  isoini  5794  oprabco  6193  ixpconstg  6681  unfiexmid  6891  undifdc  6897  sbthlemi4  6933  sbthlemi5  6934  sbthlemi6  6935  supval2ti  6968  exmidfodomrlemim  7165  suplocexprlemex  7671  eqneg  8636  zeo  9304  fseq1p1m1  10037  seq3val  10401  seqvalcd  10402  hashfzo  10744  hashxp  10748  fsumconst  11404  modfsummod  11408  telfsumo  11416  fprodconst  11570  mulgcd  11958  algcvg  11989  phiprmpw  12163  phisum  12181  strslfv3  12448  ismgmid  12618  uptx  13027  resubmet  13301  lgsval4lem  13665