Theorem eqtr4id 2286

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  iftrue  3631  iffalse  3634  difprsn1  3838  dmmptg  5265  relcoi1  5299  funimacnv  5437  dmmptd  5494  dffv3g  5671  dfimafn  5730  fvco2  5751  dfimafnf  5928  isoini  5997  iotaexel  6016  fvmpopr2d  6198  oprabco  6426  suppcofn  6479  ixpconstg  6955  unfiexmid  7191  undifdc  7197  sbthlemi4  7243  sbthlemi5  7244  sbthlemi6  7245  supval2ti  7299  exmidfodomrlemim  7517  suplocexprlemex  8053  eqneg  9026  zeo  9704  fseq1p1m1  10453  seq3val  10849  seqvalcd  10850  hashfzo  11215  hashxp  11219  hashfibclem  11234  wrdval  11255  wrdnval  11283  swrdccat3blem  11459  fsumconst  12168  modfsummod  12172  telfsumo  12180  fprodconst  12334  mulgcd  12740  algcvg  12773  phiprmpw  12947  phisum  12966  strslfv3  13345  resseqnbasd  13373  imasplusg  13575  imasmulr  13576  ismgmid  13643  gsumshift  14108  pwssnf1o  14156  pws0g  14158  dfrhm2  14402  subrg1  14480  2idlbas  14792  psrbagfi  14952  psrlinv  14968  mplbascoe  14975  mplplusgg  14987  uptx  15268  resubmet  15550  ply1termlem  15736  lgsval4lem  16013  lgsquadlem2  16080  m1lgs  16087  uspgrf1oedg  16300