Theorem coeq1i 5814

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

Syntax hints:   = wceq 1542   ∘ ccom 5635

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-co 5640

This theorem is referenced by:  coeq12i  5818  cocnvcnv1  6222  ttrclco  9639  hashgval  14295  imasdsval2  17480  prds1  20302  pf1mpf  22317  upxp  23588  uptx  23590  hoico2  31828  hoid1ri  31861  nmopcoadj2i  32173  pjclem3  32268  cycpmconjslem1  33215  cycpmconjs  33217  cyc3conja  33218  1arithidomlem2  33596  erdsze2lem2  35386  pprodcnveq  36063  diblss  41616  cononrel2  44022  trclubgNEW  44045  cortrcltrcl  44167  corclrtrcl  44168  cortrclrcl  44170  cotrclrtrcl  44171  cortrclrtrcl  44172  neicvgbex  44539  neicvgnvo  44542  dvsinax  46341