Theorem coeq1i 5801

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

Syntax hints:   = wceq 1547   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-co 5627

This theorem is referenced by:  coeq12i  5805  cocnvcnv1  6209  ttrclco  9630  hashgval  14286  imasdsval2  17471  prds1  20293  pf1mpf  22338  upxp  23606  uptx  23608  hoico2  31846  hoid1ri  31879  nmopcoadj2i  32191  pjclem3  32286  cycpmconjslem1  33235  cycpmconjs  33237  cyc3conja  33238  1arithidomlem2  33619  selvascl  33701  erdsze2lem2  35432  pprodcnveq  36109  diblss  41662  cononrel2  44039  trclubgNEW  44062  cortrcltrcl  44184  corclrtrcl  44185  cortrclrcl  44187  cotrclrtrcl  44188  cortrclrtrcl  44189  neicvgbex  44556  neicvgnvo  44559  dvsinax  46356