Theorem eqtr3di 2277

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 2233	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2275	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:  bm2.5ii  4592  resdmdfsn  5054  f0dom0  5527  f1o00  5616  fmpt  5793  fmptsn  5838  resfunexg  5870  mapsn  6854  sbthlemi4  7150  sbthlemi6  7152  pm54.43  7386  prarloclem5  7710  recexprlem1ssl  7843  recexprlem1ssu  7844  iooval2  10140  hashsng  11050  zfz1isolem1  11094  resqrexlemover  11561  isumclim3  11974  algrp1  12608  pythagtriplem1  12828  ressbasid  13143  ressval3d  13145  ressressg  13148  tangtx  15552  coskpi  15562  lgsquadlem2  15797  2omap  16530  pw1map  16532  subctctexmid  16537