Theorem coeq1d 5696

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
coeq1d	⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Proof of Theorem coeq1d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		coeq1 5692	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   = wceq 1538   ∘ ccom 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-co 5528

This theorem is referenced by:  coeq12d  5699  fcof1oinvd  7027  domss2  8660  mapen  8665  mapfien  8855  hashfacen  13808  relexpsucnnr  14376  relexpsucnnl  14381  relexpsucr  14383  relexpsucrd  14384  relexpaddnn  14402  imasval  16776  cofuass  17151  cofulid  17152  setcinv  17342  catcisolem  17358  catciso  17359  yonedalem3b  17521  gsumvalx  17878  frmdup3lem  18023  symggrplem  18041  f1omvdco2  18568  symggen  18590  psgnunilem1  18613  gsumval3  19020  gsumzf1o  19025  znval  20227  znle2  20245  psrass1lem  20615  coe1add  20893  evls1fval  20943  evl1sca  20958  evl1var  20960  evls1var  20962  pf1mpf  20976  pf1ind  20979  tcphds  23835  dvnfval  24525  hocsubdir  29568  fcoinver  30370  fcobij  30484  symgfcoeu  30776  symgcom  30777  pmtrcnel2  30784  tocyc01  30810  cycpm2tr  30811  cycpmconjv  30834  cycpmconjslem1  30846  cycpmconjslem2  30847  cycpmconjs  30848  cyc3conja  30849  reprpmtf1o  32007  hgt750lemg  32035  subfacp1lem5  32544  mrsubffval  32867  mrsubfval  32868  mrsubrn  32873  elmrsubrn  32880  upixp  35167  ltrncoidN  37424  trlcoat  38019  trlcone  38024  cdlemg47a  38030  cdlemg47  38032  ltrnco4  38035  tendovalco  38061  tendoplcbv  38071  tendopl  38072  tendoplass  38079  tendo0pl  38087  tendoipl  38093  cdlemk45  38243  cdlemk53b  38252  cdlemk55a  38255  erngdvlem3  38286  erngdvlem3-rN  38294  tendocnv  38317  dvhvaddcbv  38385  dvhvaddval  38386  dvhvaddass  38393  dicvscacl  38487  cdlemn8  38500  dihordlem7b  38511  dihopelvalcpre  38544  relexp2  40378  relexpxpnnidm  40404  relexpiidm  40405  relexpmulnn  40410  relexpaddss  40419  trclfvcom  40424  trclfvdecomr  40429  frege131d  40465  dssmap2d  40723  fundcmpsurbijinjpreimafv  43924  isomushgr  44344