Theorem coeq1i 5838

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

This proof depends on syntax axioms:   = wceq 1569   ∘ ccom 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3897  df-br 5103  df-opab 5167  df-co 5660

This theorem is used by:  coeq12i  5842  cocnvcnv1  6262  ttrclco  9726  hashgval  14484  imasdsval2  17697  prds1  20561  pf1mpf  22679  upxp  23951  uptx  23953  hoico2  32368  hoid1ri  32401  nmopcoadj2i  32713  pjclem3  32808  cycpmconjslem1  33765  cycpmconjs  33767  cyc3conja  33768  1arithidomlem2  34118  selvascl  34199  erdsze2lem2  36059  pprodcnveq  36741  diblss  42336  cononrel2  44704  trclubgNEW  44727  cortrcltrcl  44849  corclrtrcl  44850  cortrclrcl  44852  cotrclrtrcl  44853  cortrclrtrcl  44854  neicvgbex  45221  neicvgnvo  45224  dvsinax  47031