Theorem eqtr4id 2290

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr4id.2	⊢ 𝐴 = 𝐵
eqtr4id.1	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eqtr4id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4id

Step	Hyp	Ref	Expression
1		eqtr4id.1	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
2		eqtr4id.2	. . 3 ⊢ 𝐴 = 𝐵
3	2	eqcomi 2242	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2288	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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  5285  relcoi1  5319  funimacnv  5457  dmmptd  5514  dffv3g  5691  dfimafn  5751  fvco2  5774  dfimafnf  5955  isoini  6024  iotaexel  6043  fvmpopr2d  6225  oprabco  6453  suppcofn  6506  ixpconstg  6989  unfiexmid  7225  undifdc  7231  sbthlemi4  7277  sbthlemi5  7278  sbthlemi6  7279  supval2ti  7335  exmidfodomrlemim  7553  suplocexprlemex  8089  eqneg  9063  zeo  9753  fseq1p1m1  10503  seq3val  10899  seqvalcd  10900  hashfzo  11265  hashxp  11269  hashfibclem  11284  wrdval  11309  wrdnval  11337  swrdccat3blem  11513  fsumconst  12223  modfsummod  12227  telfsumo  12235  fprodconst  12389  mulgcd  12795  algcvg  12828  phiprmpw  13002  phisum  13021  strslfv3  13400  resseqnbasd  13429  imasplusg  13631  imasmulr  13632  ismgmid  13699  gzsumshift  14151  pwssnf1o  14213  pws0g  14215  dfrhm2  14463  subrg1  14541  2idlbas  14854  rnascl  15036  psrbagfi  15061  psrlinv  15077  mplbascoe  15084  mplplusgg  15096  uptx  15377  resubmet  15659  ply1termlem  15845  birthdaylem1g  16093  birthdaylem2  16094  lgsval4lem  16142  lgsquadlem2  16209  m1lgs  16216  uspgrf1oedg  16429