Theorem coeq1i 5837

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-co 5660

This theorem is used by:  coeq12i  5841  cocnvcnv1  6258  ttrclco  9712  hashgval  14470  imasdsval2  17681  prds1  20545  pf1mpf  22663  upxp  23935  uptx  23937  hoico2  32352  hoid1ri  32385  nmopcoadj2i  32697  pjclem3  32792  cycpmconjslem1  33708  cycpmconjs  33710  cyc3conja  33711  1arithidomlem2  34061  selvascl  34142  erdsze2lem2  35948  pprodcnveq  36625  diblss  42207  cononrel2  44580  trclubgNEW  44603  cortrcltrcl  44725  corclrtrcl  44726  cortrclrcl  44728  cotrclrtrcl  44729  cortrclrtrcl  44730  neicvgbex  45097  neicvgnvo  45100  dvsinax  46892