Theorem eqtr4id 2229

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  iftrue  3539  iffalse  3542  difprsn1  3731  dmmptg  5123  relcoi1  5157  funimacnv  5289  dmmptd  5343  dffv3g  5508  dfimafn  5561  fvco2  5582  isoini  5814  oprabco  6213  ixpconstg  6702  unfiexmid  6912  undifdc  6918  sbthlemi4  6954  sbthlemi5  6955  sbthlemi6  6956  supval2ti  6989  exmidfodomrlemim  7195  suplocexprlemex  7716  eqneg  8683  zeo  9352  fseq1p1m1  10087  seq3val  10451  seqvalcd  10452  hashfzo  10793  hashxp  10797  fsumconst  11453  modfsummod  11457  telfsumo  11465  fprodconst  11619  mulgcd  12007  algcvg  12038  phiprmpw  12212  phisum  12230  strslfv3  12498  resseqnbasd  12522  ismgmid  12726  uptx  13556  resubmet  13830  lgsval4lem  14194