Theorem eqtr2d 1129

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
eqtr2d	⊢ (φ → C = A)

Proof of Theorem eqtr2d

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

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  sbthlem3 3351  aceq6b 3565  divadddivt 4264  infxpidmlem4 4936  chsupid 5312  osumlem2 5531  pjot 5561

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