Theorem eqtr3di 2252

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr3di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr3di.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3di	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3di

Step	Hyp	Ref	Expression
1		eqtr3di.2	. . 3 ⊢ 𝐴 = 𝐶
2	1	eqcomi 2208	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2250	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  bm2.5ii  4543  resdmdfsn  5001  f0dom0  5468  f1o00  5556  fmpt  5729  fmptsn  5772  resfunexg  5804  mapsn  6776  sbthlemi4  7061  sbthlemi6  7063  pm54.43  7297  prarloclem5  7612  recexprlem1ssl  7745  recexprlem1ssu  7746  iooval2  10036  hashsng  10941  zfz1isolem1  10983  resqrexlemover  11263  isumclim3  11676  algrp1  12310  pythagtriplem1  12530  ressbasid  12844  ressval3d  12846  ressressg  12849  tangtx  15252  coskpi  15262  lgsquadlem2  15497  2omap  15865  subctctexmid  15870