Theorem coeq1i 5848

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5109  df-opab 5174  df-co 5667

This theorem is used by:  coeq12i  5852  cocnvcnv1  6278  coires2  6289  ttrclco  9756  hashgval  14518  imasdsval2  17738  prds1  20603  pf1mpf  22725  upxp  23997  uptx  23999  hoico2  32416  hoid1ri  32449  nmopcoadj2i  32761  pjclem3  32856  cycpmconjslem1  33814  cycpmconjs  33816  cyc3conja  33817  1arithidomlem2  34172  selvascl  34260  erdsze2lem2  36177  pprodcnveq  36860  coidmid  38225  nvo3  38230  diblss  42493  cononrel2  44856  trclubgNEW  44879  cortrcltrcl  45001  corclrtrcl  45002  cortrclrcl  45004  cotrclrtrcl  45005  cortrclrtrcl  45006  neicvgbex  45373  neicvgnvo  45376  dvsinax  47196