Theorem eqtr4id 2281

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 2233	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2279	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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  3608  iffalse  3611  difprsn1  3810  dmmptg  5232  relcoi1  5266  funimacnv  5403  dmmptd  5460  dffv3g  5631  dfimafn  5690  fvco2  5711  isoini  5954  iotaexel  5971  fvmpopr2d  6153  oprabco  6377  ixpconstg  6871  unfiexmid  7105  undifdc  7111  sbthlemi4  7153  sbthlemi5  7154  sbthlemi6  7155  supval2ti  7188  exmidfodomrlemim  7405  suplocexprlemex  7935  eqneg  8905  zeo  9578  fseq1p1m1  10322  seq3val  10715  seqvalcd  10716  hashfzo  11079  hashxp  11083  wrdval  11109  wrdnval  11137  swrdccat3blem  11313  fsumconst  12008  modfsummod  12012  telfsumo  12020  fprodconst  12174  mulgcd  12580  algcvg  12613  phiprmpw  12787  phisum  12806  strslfv3  13121  resseqnbasd  13149  pwssnf1o  13374  imasplusg  13384  imasmulr  13385  ismgmid  13453  pws0g  13527  dfrhm2  14161  subrg1  14238  2idlbas  14522  psrbagfi  14680  psrlinv  14691  mplbascoe  14698  mplplusgg  14710  uptx  14991  resubmet  15273  ply1termlem  15459  lgsval4lem  15733  lgsquadlem2  15800  m1lgs  15807  uspgrf1oedg  16020  gsumgfsumlem  16633