Theorem coeq1i 5802

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

Syntax hints:   = wceq 1540   ∘ ccom 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920  df-br 5093  df-opab 5155  df-co 5628

This theorem is referenced by:  coeq12i  5806  cocnvcnv1  6206  ttrclco  9614  hashgval  14240  imasdsval2  17420  prds1  20208  pf1mpf  22237  upxp  23508  uptx  23510  hoico2  31701  hoid1ri  31734  nmopcoadj2i  32046  pjclem3  32141  cycpmconjslem1  33096  cycpmconjs  33098  cyc3conja  33099  1arithidomlem2  33473  erdsze2lem2  35177  pprodcnveq  35857  diblss  41149  cononrel2  43568  trclubgNEW  43591  cortrcltrcl  43713  corclrtrcl  43714  cortrclrcl  43716  cotrclrtrcl  43717  cortrclrtrcl  43718  neicvgbex  44085  neicvgnvo  44088  dvsinax  45894