Theorem coeq1i 5858

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

Syntax hints:   = wceq 1542   ∘ ccom 5680

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-br 5149  df-opab 5211  df-co 5685

This theorem is referenced by:  coeq12i  5862  cocnvcnv1  6254  ttrclco  9710  hashgval  14290  imasdsval2  17459  prds1  20130  pf1mpf  21863  upxp  23119  uptx  23121  hoico2  30998  hoid1ri  31031  nmopcoadj2i  31343  pjclem3  31438  cycpmconjslem1  32301  cycpmconjs  32303  cyc3conja  32304  erdsze2lem2  34184  pprodcnveq  34844  diblss  40030  cononrel2  42332  trclubgNEW  42355  cortrcltrcl  42477  corclrtrcl  42478  cortrclrcl  42480  cotrclrtrcl  42481  cortrclrtrcl  42482  neicvgbex  42849  neicvgnvo  42852  dvsinax  44616