Theorem eqtr4id 2281

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  iftrue  3607  iffalse  3610  difprsn1  3807  dmmptg  5226  relcoi1  5260  funimacnv  5397  dmmptd  5454  dffv3g  5625  dfimafn  5684  fvco2  5705  isoini  5948  iotaexel  5965  fvmpopr2d  6147  oprabco  6369  ixpconstg  6862  unfiexmid  7091  undifdc  7097  sbthlemi4  7138  sbthlemi5  7139  sbthlemi6  7140  supval2ti  7173  exmidfodomrlemim  7390  suplocexprlemex  7920  eqneg  8890  zeo  9563  fseq1p1m1  10302  seq3val  10694  seqvalcd  10695  hashfzo  11057  hashxp  11061  wrdval  11087  wrdnval  11115  swrdccat3blem  11286  fsumconst  11980  modfsummod  11984  telfsumo  11992  fprodconst  12146  mulgcd  12552  algcvg  12585  phiprmpw  12759  phisum  12778  strslfv3  13093  resseqnbasd  13121  pwssnf1o  13346  imasplusg  13356  imasmulr  13357  ismgmid  13425  pws0g  13499  dfrhm2  14133  subrg1  14210  2idlbas  14494  psrbagfi  14652  psrlinv  14663  mplbascoe  14670  mplplusgg  14682  uptx  14963  resubmet  15245  ply1termlem  15431  lgsval4lem  15705  lgsquadlem2  15772  m1lgs  15779  uspgrf1oedg  15989