Theorem coeq1i 5806

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 5804	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)

Syntax hints:   = wceq 1541   ∘ ccom 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-co 5631

This theorem is referenced by:  coeq12i  5810  cocnvcnv1  6214  ttrclco  9625  hashgval  14254  imasdsval2  17435  prds1  20256  pf1mpf  22294  upxp  23565  uptx  23567  hoico2  31781  hoid1ri  31814  nmopcoadj2i  32126  pjclem3  32221  cycpmconjslem1  33185  cycpmconjs  33187  cyc3conja  33188  1arithidomlem2  33566  erdsze2lem2  35347  pprodcnveq  36024  diblss  41369  cononrel2  43778  trclubgNEW  43801  cortrcltrcl  43923  corclrtrcl  43924  cortrclrcl  43926  cotrclrtrcl  43927  cortrclrtrcl  43928  neicvgbex  44295  neicvgnvo  44298  dvsinax  46099