Theorem coeq1i 5809

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

Syntax hints:   = wceq 1542   ∘ ccom 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-co 5634

This theorem is referenced by:  coeq12i  5813  cocnvcnv1  6217  ttrclco  9633  hashgval  14289  imasdsval2  17474  prds1  20296  pf1mpf  22330  upxp  23601  uptx  23603  hoico2  31846  hoid1ri  31879  nmopcoadj2i  32191  pjclem3  32286  cycpmconjslem1  33233  cycpmconjs  33235  cyc3conja  33236  1arithidomlem2  33614  erdsze2lem2  35405  pprodcnveq  36082  diblss  41633  cononrel2  44043  trclubgNEW  44066  cortrcltrcl  44188  corclrtrcl  44189  cortrclrcl  44191  cotrclrtrcl  44192  cortrclrtrcl  44193  neicvgbex  44560  neicvgnvo  44563  dvsinax  46362