Theorem eqtr4id 2290

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  iftrue  3645  iffalse  3648  difprsn1  3854  dmmptg  5288  relcoi1  5322  funimacnv  5460  dmmptd  5517  dffv3g  5694  dfimafn  5754  fvco2  5777  dfimafnf  5958  isoini  6027  iotaexel  6046  fvmpopr2d  6228  oprabco  6457  suppcofn  6510  ixpconstg  6995  unfiexmid  7231  undifdc  7237  sbthlemi4  7284  sbthlemi5  7285  sbthlemi6  7286  supval2ti  7341  exmidfodomrlemim  7559  suplocexprlemex  8095  eqneg  9070  zeo  9761  fseq1p1m1  10517  seq3val  10917  seqvalcd  10918  hashfzo  11284  hashxp  11288  hashfibclem  11303  wrdval  11328  wrdnval  11356  swrdccat3blem  11532  fsumconst  12245  modfsummod  12249  telfsumo  12257  fprodconst  12411  mulgcd  12817  algcvg  12850  phiprmpw  13028  phisum  13047  strslfv3  13455  resseqnbasd  13485  imasplusg  13687  imasmulr  13688  ismgmid  13755  gzsumshift  14238  pwssnf1o  14317  pws0g  14319  dfrhm2  14569  subrg1  14647  2idlbas  14960  rnascl  15142  psrbagfi  15166  psrlinv  15203  mplbas  15223  mplplusgg  15236  uptx  15517  resubmet  15799  ply1termlem  15985  birthdaylem1g  16242  birthdaylem2  16243  chtqub  16313  lgsval4lem  16352  lgsquadlem2  16419  m1lgs  16426  uspgrf1oedg  16639