Theorem coeq1i 5839

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-co 5664

This theorem is used by:  coeq12i  5843  cocnvcnv1  6254  ttrclco  9697  hashgval  14397  imasdsval2  17602  prds1  20463  pf1mpf  22577  upxp  23849  uptx  23851  hoico2  32238  hoid1ri  32271  nmopcoadj2i  32583  pjclem3  32678  cycpmconjslem1  33594  cycpmconjs  33596  cyc3conja  33597  1arithidomlem2  33946  selvascl  34027  erdsze2lem2  35783  pprodcnveq  36460  diblss  42043  cononrel2  44435  trclubgNEW  44458  cortrcltrcl  44580  corclrtrcl  44581  cortrclrcl  44583  cotrclrtrcl  44584  cortrclrtrcl  44585  neicvgbex  44952  neicvgnvo  44955  dvsinax  46741