Theorem coeq1d 5193

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 5189	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   = wceq 1474   ∘ ccom 5032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-in 3546  df-ss 3553  df-br 4578  df-opab 4638  df-co 5037

This theorem is referenced by:  coeq12d  5196  fcof1oinvd  6426  domss2  7981  mapen  7986  mapfien  8173  hashfacen  13047  relexpsucnnr  13559  relexpsucr  13563  relexpsucnnl  13566  relexpaddnn  13585  imasval  15940  cofuass  16318  cofulid  16319  setcinv  16509  catcisolem  16525  catciso  16526  yonedalem3b  16688  gsumvalx  17039  frmdup3lem  17172  symggrp  17589  f1omvdco2  17637  symggen  17659  psgnunilem1  17682  gsumval3  18077  gsumzf1o  18082  psrass1lem  19144  coe1add  19401  evls1fval  19451  evl1sca  19465  evl1var  19467  evls1var  19469  pf1mpf  19483  pf1ind  19486  znval  19647  znle2  19666  tchds  22759  dvnfval  23408  hocsubdir  27834  fcoinver  28604  fcobij  28694  symgfcoeu  28982  subfacp1lem5  30226  mrsubffval  30464  mrsubfval  30465  mrsubrn  30470  elmrsubrn  30477  upixp  32497  ltrncoidN  34235  trlcoat  34832  trlcone  34837  cdlemg47a  34843  cdlemg47  34845  ltrnco4  34848  tendovalco  34874  tendoplcbv  34884  tendopl  34885  tendoplass  34892  tendo0pl  34900  tendoipl  34906  cdlemk45  35056  cdlemk53b  35065  cdlemk55a  35068  erngdvlem3  35099  erngdvlem3-rN  35107  tendocnv  35131  dvhvaddcbv  35199  dvhvaddval  35200  dvhvaddass  35207  dicvscacl  35301  cdlemn8  35314  dihordlem7b  35325  dihopelvalcpre  35358  relexp2  36791  relexpxpnnidm  36817  relexpiidm  36818  relexpmulnn  36823  relexpaddss  36832  trclfvcom  36837  trclfvdecomr  36842  frege131d  36878  dssmap2d  37139