Theorem eqtr3d 1130

Description: An equality transitivity equality deduction.

Hypotheses

Ref	Expression
eqtr3d.1	⊢ (φ → A = B)
eqtr3d.2	⊢ (φ → A = C)

Assertion

Ref	Expression
eqtr3d	⊢ (φ → B = C)

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 ⊢ (φ → A = B)
2	1	cleqcomd 1106	. 2 ⊢ (φ → B = A)
3		eqtr3d.2	. 2 ⊢ (φ → A = C)
4	2, 3	eqtrd 1128	1 ⊢ (φ → B = C)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  3eqtr3d 1133  f00 2773  f1imacnv 2814  f1ococnv1 2818  caoprmo 3084  map0b 3267  mapsn 3269  en1 3331  ssenen 3399  1qec 3862  halfpq 3876  pn0sr 4004  mulgt0sr 4008  npcant 4162  subsubt 4203  divmuldivt 4263  divdivdivt 4265  znnsubt 4595  qrecclt 4646  expaddt 4698  ruclem8 4892  hvaddid2t 5003  hvmul0t 5004  hvnegidt 5006  hvm1negt 5007  hvsubaddeqt 5019  chdmj1t 5442  h1de2b 5459  spansncol 5473  h1datom 5483  5oalem1 5544  3oalem2 5553  pjclem4 5653  pj3s 5659  sto1 5677  cvexchlem 5759  mdsymlem1 5776

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org