Theorem coeq1i 5826

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

Syntax hints:   = wceq 1540   ∘ ccom 5645

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-co 5650

This theorem is referenced by:  coeq12i  5830  cocnvcnv1  6233  ttrclco  9678  hashgval  14305  imasdsval2  17486  prds1  20239  pf1mpf  22246  upxp  23517  uptx  23519  hoico2  31693  hoid1ri  31726  nmopcoadj2i  32038  pjclem3  32133  cycpmconjslem1  33118  cycpmconjs  33120  cyc3conja  33121  1arithidomlem2  33514  erdsze2lem2  35198  pprodcnveq  35878  diblss  41171  cononrel2  43591  trclubgNEW  43614  cortrcltrcl  43736  corclrtrcl  43737  cortrclrcl  43739  cotrclrtrcl  43740  cortrclrtrcl  43741  neicvgbex  44108  neicvgnvo  44111  dvsinax  45918