Theorem coeq1i 5872

Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
coeq1i	⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)

Proof of Theorem coeq1i

Step	Hyp	Ref	Expression
1		coeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		coeq1 5870	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)

Syntax hints:   = wceq 1536   ∘ ccom 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-co 5697

This theorem is referenced by:  coeq12i  5876  cocnvcnv1  6278  ttrclco  9755  hashgval  14368  imasdsval2  17562  prds1  20336  pf1mpf  22371  upxp  23646  uptx  23648  hoico2  31785  hoid1ri  31818  nmopcoadj2i  32130  pjclem3  32225  cycpmconjslem1  33156  cycpmconjs  33158  cyc3conja  33159  1arithidomlem2  33543  erdsze2lem2  35188  pprodcnveq  35864  diblss  41152  cononrel2  43584  trclubgNEW  43607  cortrcltrcl  43729  corclrtrcl  43730  cortrclrcl  43732  cotrclrtrcl  43733  cortrclrtrcl  43734  neicvgbex  44101  neicvgnvo  44104  dvsinax  45868