Theorem coeq1i 5823

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

Syntax hints:   = wceq 1540   ∘ ccom 5642

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 3931  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  coeq12i  5827  cocnvcnv1  6230  ttrclco  9671  hashgval  14298  imasdsval2  17479  prds1  20232  pf1mpf  22239  upxp  23510  uptx  23512  hoico2  31686  hoid1ri  31719  nmopcoadj2i  32031  pjclem3  32126  cycpmconjslem1  33111  cycpmconjs  33113  cyc3conja  33114  1arithidomlem2  33507  erdsze2lem2  35191  pprodcnveq  35871  diblss  41164  cononrel2  43584  trclubgNEW  43607  cortrcltrcl  43729  corclrtrcl  43730  cortrclrcl  43732  cotrclrtrcl  43733  cortrclrtrcl  43734  neicvgbex  44101  neicvgnvo  44104  dvsinax  45911