Theorem coeq1i 5831

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

Syntax hints:   = wceq 1560   ∘ ccom 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5101  df-opab 5163  df-co 5656

This theorem is referenced by:  coeq12i  5835  cocnvcnv1  6245  ttrclco  9673  hashgval  14346  imasdsval2  17546  prds1  20367  pf1mpf  22412  upxp  23680  uptx  23682  hoico2  31957  hoid1ri  31990  nmopcoadj2i  32302  pjclem3  32397  cycpmconjslem1  33331  cycpmconjs  33333  cyc3conja  33334  1arithidomlem2  33729  selvascl  33811  erdsze2lem2  35551  pprodcnveq  36228  diblss  41791  cononrel2  44168  trclubgNEW  44191  cortrcltrcl  44313  corclrtrcl  44314  cortrclrcl  44316  cotrclrtrcl  44317  cortrclrtrcl  44318  neicvgbex  44685  neicvgnvo  44688  dvsinax  46484