Theorem coeq1i 5757

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

Syntax hints:   = wceq 1539   ∘ ccom 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-co 5589

This theorem is referenced by:  coeq12i  5761  cocnvcnv1  6150  hashgval  13975  imasdsval2  17144  prds1  19768  pf1mpf  21428  upxp  22682  uptx  22684  hoico2  30020  hoid1ri  30053  nmopcoadj2i  30365  pjclem3  30460  cycpmconjslem1  31323  cycpmconjs  31325  cyc3conja  31326  erdsze2lem2  33066  ttrclco  33704  pprodcnveq  34112  diblss  39111  cononrel2  41092  trclubgNEW  41115  cortrcltrcl  41237  corclrtrcl  41238  cortrclrcl  41240  cotrclrtrcl  41241  cortrclrtrcl  41242  neicvgbex  41611  neicvgnvo  41614  dvsinax  43344