Theorem coeq1i 5860

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

Syntax hints:   = wceq 1542   ∘ ccom 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686

This theorem is referenced by:  coeq12i  5864  cocnvcnv1  6257  ttrclco  9713  hashgval  14293  imasdsval2  17462  prds1  20136  pf1mpf  21871  upxp  23127  uptx  23129  hoico2  31010  hoid1ri  31043  nmopcoadj2i  31355  pjclem3  31450  cycpmconjslem1  32313  cycpmconjs  32315  cyc3conja  32316  erdsze2lem2  34195  pprodcnveq  34855  diblss  40041  cononrel2  42346  trclubgNEW  42369  cortrcltrcl  42491  corclrtrcl  42492  cortrclrcl  42494  cotrclrtrcl  42495  cortrclrtrcl  42496  neicvgbex  42863  neicvgnvo  42866  dvsinax  44629