Theorem 3eqtr3a 2295

Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)

Hypotheses

Ref	Expression
3eqtr3a.1	⊢ 𝐴 = 𝐵
3eqtr3a.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3a.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3a	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3a

Step	Hyp	Ref	Expression
1		3eqtr3a.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		3eqtr3a.1	. . 3 ⊢ 𝐴 = 𝐵
3		3eqtr3a.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	eqtrid 2283	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2273	1 ⊢ (𝜑 → 𝐶 = 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  uneqin  3482  coi2  5307  foima  5623  f1imacnv  5659  fvsnun2  5916  fnsnsplitdc  6783  phplem4  7162  phplem4on  7175  halfnqq  7783  resqrexlemcalc1  11801  absefib  12562  efieq1re  12563  restopnb  15424  cnmpt2t  15536  sineq0re  16093  reeflog  16109  rpcxpsqrt  16174