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 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  iftrue  3645  iffalse  3648  difprsn1  3852  dmmptg  5283  relcoi1  5317  funimacnv  5455  dmmptd  5512  dffv3g  5689  dfimafn  5748  fvco2  5771  dfimafnf  5949  isoini  6018  iotaexel  6037  fvmpopr2d  6219  oprabco  6447  suppcofn  6500  ixpconstg  6983  unfiexmid  7219  undifdc  7225  sbthlemi4  7271  sbthlemi5  7272  sbthlemi6  7273  supval2ti  7329  exmidfodomrlemim  7547  suplocexprlemex  8083  eqneg  9056  zeo  9734  fseq1p1m1  10484  seq3val  10880  seqvalcd  10881  hashfzo  11246  hashxp  11250  hashfibclem  11265  wrdval  11290  wrdnval  11318  swrdccat3blem  11494  fsumconst  12204  modfsummod  12208  telfsumo  12216  fprodconst  12370  mulgcd  12776  algcvg  12809  phiprmpw  12983  phisum  13002  strslfv3  13381  resseqnbasd  13410  imasplusg  13612  imasmulr  13613  ismgmid  13680  gzsumshift  14132  pwssnf1o  14194  pws0g  14196  dfrhm2  14444  subrg1  14522  2idlbas  14835  rnascl  15017  psrbagfi  15042  psrlinv  15058  mplbascoe  15065  mplplusgg  15077  uptx  15358  resubmet  15640  ply1termlem  15826  birthdaylem1g  16070  birthdaylem2  16071  lgsval4lem  16113  lgsquadlem2  16180  m1lgs  16187  uspgrf1oedg  16400