Theorem coeq1i 5870

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

Syntax hints:   = wceq 1540   ∘ ccom 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694

This theorem is referenced by:  coeq12i  5874  cocnvcnv1  6277  ttrclco  9758  hashgval  14372  imasdsval2  17561  prds1  20320  pf1mpf  22356  upxp  23631  uptx  23633  hoico2  31776  hoid1ri  31809  nmopcoadj2i  32121  pjclem3  32216  cycpmconjslem1  33174  cycpmconjs  33176  cyc3conja  33177  1arithidomlem2  33564  erdsze2lem2  35209  pprodcnveq  35884  diblss  41172  cononrel2  43608  trclubgNEW  43631  cortrcltrcl  43753  corclrtrcl  43754  cortrclrcl  43756  cotrclrtrcl  43757  cortrclrtrcl  43758  neicvgbex  44125  neicvgnvo  44128  dvsinax  45928