Theorem coeq1i 5846

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

Syntax hints:   = wceq 1567   ∘ ccom 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-co 5671

This theorem is referenced by:  coeq12i  5850  cocnvcnv1  6260  ttrclco  9686  hashgval  14368  imasdsval2  17569  prds1  20403  pf1mpf  22480  upxp  23748  uptx  23750  hoico2  32049  hoid1ri  32082  nmopcoadj2i  32394  pjclem3  32489  cycpmconjslem1  33414  cycpmconjs  33416  cyc3conja  33417  1arithidomlem2  33770  selvascl  33851  erdsze2lem2  35594  pprodcnveq  36271  diblss  41833  cononrel2  44212  trclubgNEW  44235  cortrcltrcl  44357  corclrtrcl  44358  cortrclrcl  44360  cotrclrtrcl  44361  cortrclrtrcl  44362  neicvgbex  44729  neicvgnvo  44732  dvsinax  46518