Theorem coeq1d 5815

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

Syntax hints:   → wi 4   = 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:  coeq12d  5818  fcof1oinvd  7250  domss2  9077  mapen  9082  mapfien  9335  hashfacen  14395  relexpsucnnr  14967  relexpsucnnl  14972  relexpsucr  14974  relexpsucrd  14975  relexpaddnn  14993  imasval  17450  cofuass  17827  cofulid  17828  setcinv  18028  catcisolem  18048  catciso  18049  yonedalem3b  18216  gsumvalx  18579  frmdup3lem  18769  symggrplem  18787  f1omvdco2  19354  symggen  19376  psgnunilem1  19399  gsumval3  19813  gsumzf1o  19818  znval  21421  znle2  21439  psrass1lem  21817  coe1add  22126  evls1fval  22182  evl1sca  22197  evl1var  22199  evls1var  22201  pf1mpf  22215  pf1ind  22218  tcphds  25107  dvnfval  25800  hocsubdir  31687  fcoinver  32506  fcobij  32618  ccatws1f1olast  32847  symgfcoeu  33012  symgcom  33013  pmtrcnel2  33020  tocyc01  33048  cycpm2tr  33049  cycpmconjv  33072  cycpmconjslem1  33084  cycpmconjslem2  33085  cycpmconjs  33086  cyc3conja  33087  1arithidomlem2  33480  reprpmtf1o  34590  hgt750lemg  34618  subfacp1lem5  35144  mrsubffval  35467  mrsubfval  35468  mrsubrn  35473  elmrsubrn  35480  upixp  37696  ltrncoidN  40095  trlcoat  40690  trlcone  40695  cdlemg47a  40701  cdlemg47  40703  ltrnco4  40706  tendovalco  40732  tendoplcbv  40742  tendopl  40743  tendoplass  40750  tendo0pl  40758  tendoipl  40764  cdlemk45  40914  cdlemk53b  40923  cdlemk55a  40926  erngdvlem3  40957  erngdvlem3-rN  40965  tendocnv  40988  dvhvaddcbv  41056  dvhvaddval  41057  dvhvaddass  41064  dicvscacl  41158  cdlemn8  41171  dihordlem7b  41182  dihopelvalcpre  41215  aks6d1c6lem5  42138  relexp2  43639  relexpxpnnidm  43665  relexpiidm  43666  relexpmulnn  43671  relexpaddss  43680  trclfvcom  43685  trclfvdecomr  43690  frege131d  43726  dssmap2d  43984  fundcmpsurbijinjpreimafv  47381  gricushgr  47890  prcof21a  49353