Theorem coeq1i 5816

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

Syntax hints:   = wceq 1542   ∘ ccom 5636

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 3920  df-br 5101  df-opab 5163  df-co 5641

This theorem is referenced by:  coeq12i  5820  cocnvcnv1  6224  ttrclco  9639  hashgval  14268  imasdsval2  17449  prds1  20270  pf1mpf  22308  upxp  23579  uptx  23581  hoico2  31845  hoid1ri  31878  nmopcoadj2i  32190  pjclem3  32285  cycpmconjslem1  33248  cycpmconjs  33250  cyc3conja  33251  1arithidomlem2  33629  erdsze2lem2  35420  pprodcnveq  36097  diblss  41546  cononrel2  43951  trclubgNEW  43974  cortrcltrcl  44096  corclrtrcl  44097  cortrclrcl  44099  cotrclrtrcl  44100  cortrclrtrcl  44101  neicvgbex  44468  neicvgnvo  44471  dvsinax  46271