Theorem coeq1i 5813

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

Syntax hints:   = wceq 1540   ∘ ccom 5635

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-co 5640

This theorem is referenced by:  coeq12i  5817  cocnvcnv1  6218  ttrclco  9647  hashgval  14274  imasdsval2  17455  prds1  20208  pf1mpf  22215  upxp  23486  uptx  23488  hoico2  31659  hoid1ri  31692  nmopcoadj2i  32004  pjclem3  32099  cycpmconjslem1  33084  cycpmconjs  33086  cyc3conja  33087  1arithidomlem2  33480  erdsze2lem2  35164  pprodcnveq  35844  diblss  41137  cononrel2  43557  trclubgNEW  43580  cortrcltrcl  43702  corclrtrcl  43703  cortrclrcl  43705  cotrclrtrcl  43706  cortrclrtrcl  43707  neicvgbex  44074  neicvgnvo  44077  dvsinax  45884