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  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  6994  unfiexmid  7230  undifdc  7236  sbthlemi4  7283  sbthlemi5  7284  sbthlemi6  7285  supval2ti  7342  exmidfodomrlemim  7560  suplocexprlemex  8096  eqneg  9071  zeo  9763  fseq1p1m1  10519  seq3val  10919  seqvalcd  10920  hashfzo  11286  hashxp  11290  hashfibclem  11305  wrdval  11330  wrdnval  11358  swrdccat3blem  11534  fsumconst  12247  modfsummod  12251  telfsumo  12259  fprodconst  12413  mulgcd  12819  algcvg  12852  phiprmpw  13030  phisum  13049  strslfv3  13457  resseqnbasd  13487  imasplusg  13689  imasmulr  13690  ismgmid  13757  gzsumshift  14240  pwssnf1o  14319  pws0g  14321  dfrhm2  14571  subrg1  14649  2idlbas  14962  rnascl  15144  psrbagfi  15168  psrlinv  15199  mplbascoe  15219  mplplusgg  15231  uptx  15512  resubmet  15794  ply1termlem  15980  birthdaylem1g  16237  birthdaylem2  16238  chtqub  16308  lgsval4lem  16347  lgsquadlem2  16414  m1lgs  16421  uspgrf1oedg  16634