Theorem eqtr3di 2205

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 2161	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2203	1 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150

This theorem is referenced by:  bm2.5ii  4458  resdmdfsn  4912  f0dom0  5366  f1o00  5452  fmpt  5620  fmptsn  5659  resfunexg  5691  mapsn  6638  sbthlemi4  6907  sbthlemi6  6909  pm54.43  7128  prarloclem5  7423  recexprlem1ssl  7556  recexprlem1ssu  7557  iooval2  9826  hashsng  10684  zfz1isolem1  10723  resqrexlemover  10922  isumclim3  11332  algrp1  11939  pythagtriplem1  12156  tangtx  13255  coskpi  13265  subctctexmid  13670