Theorem coeq1i 5845

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

Syntax hints:   = wceq 1570   ∘ ccom 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-co 5670

This theorem is referenced by:  coeq12i  5849  cocnvcnv1  6259  ttrclco  9683  hashgval  14365  imasdsval2  17565  prds1  20400  pf1mpf  22512  upxp  23780  uptx  23782  hoico2  32109  hoid1ri  32142  nmopcoadj2i  32454  pjclem3  32549  cycpmconjslem1  33474  cycpmconjs  33476  cyc3conja  33477  1arithidomlem2  33826  selvascl  33907  erdsze2lem2  35696  pprodcnveq  36373  diblss  41944  cononrel2  44321  trclubgNEW  44344  cortrcltrcl  44466  corclrtrcl  44467  cortrclrcl  44469  cotrclrtrcl  44470  cortrclrtrcl  44471  neicvgbex  44838  neicvgnvo  44841  dvsinax  46627