Theorem eqtr4id 2284

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 2236	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2282	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 2214

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

This theorem is referenced by:  iftrue  3626  iffalse  3629  difprsn1  3832  dmmptg  5259  relcoi1  5293  funimacnv  5431  dmmptd  5488  dffv3g  5665  dfimafn  5724  fvco2  5745  isoini  5990  iotaexel  6007  fvmpopr2d  6189  oprabco  6412  suppcofn  6465  ixpconstg  6941  unfiexmid  7177  undifdc  7183  sbthlemi4  7229  sbthlemi5  7230  sbthlemi6  7231  supval2ti  7285  exmidfodomrlemim  7503  suplocexprlemex  8033  eqneg  9002  zeo  9679  fseq1p1m1  10424  seq3val  10818  seqvalcd  10819  hashfzo  11182  hashxp  11186  hashfibclem  11199  wrdval  11220  wrdnval  11248  swrdccat3blem  11424  fsumconst  12133  modfsummod  12137  telfsumo  12145  fprodconst  12299  mulgcd  12705  algcvg  12738  phiprmpw  12912  phisum  12931  strslfv3  13247  resseqnbasd  13275  pwssnf1o  13500  imasplusg  13510  imasmulr  13511  ismgmid  13579  pws0g  13653  dfrhm2  14288  subrg1  14365  2idlbas  14650  psrbagfi  14810  psrlinv  14826  mplbascoe  14833  mplplusgg  14845  uptx  15126  resubmet  15408  ply1termlem  15594  lgsval4lem  15871  lgsquadlem2  15938  m1lgs  15945  uspgrf1oedg  16158  gsumgfsumlem  16851