Theorem coeq1i 5884

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

Syntax hints:   = wceq 1537   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  coeq12i  5888  cocnvcnv1  6288  ttrclco  9787  hashgval  14382  imasdsval2  17576  prds1  20346  pf1mpf  22377  upxp  23652  uptx  23654  hoico2  31789  hoid1ri  31822  nmopcoadj2i  32134  pjclem3  32229  cycpmconjslem1  33147  cycpmconjs  33149  cyc3conja  33150  1arithidomlem2  33529  erdsze2lem2  35172  pprodcnveq  35847  diblss  41127  cononrel2  43557  trclubgNEW  43580  cortrcltrcl  43702  corclrtrcl  43703  cortrclrcl  43705  cotrclrtrcl  43706  cortrclrtrcl  43707  neicvgbex  44074  neicvgnvo  44077  dvsinax  45834