Theorem coeq1i 5768

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

Syntax hints:   = wceq 1539   ∘ ccom 5593

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075  df-opab 5137  df-co 5598

This theorem is referenced by:  coeq12i  5772  cocnvcnv1  6161  ttrclco  9476  hashgval  14047  imasdsval2  17227  prds1  19853  pf1mpf  21518  upxp  22774  uptx  22776  hoico2  30119  hoid1ri  30152  nmopcoadj2i  30464  pjclem3  30559  cycpmconjslem1  31421  cycpmconjs  31423  cyc3conja  31424  erdsze2lem2  33166  pprodcnveq  34185  diblss  39184  cononrel2  41203  trclubgNEW  41226  cortrcltrcl  41348  corclrtrcl  41349  cortrclrcl  41351  cotrclrtrcl  41352  cortrclrtrcl  41353  neicvgbex  41722  neicvgnvo  41725  dvsinax  43454