Theorem coeq1d 5485

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

Syntax hints:   → wi 4   = wceq 1637   ∘ ccom 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-in 3776  df-ss 3783  df-br 4845  df-opab 4907  df-co 5320

This theorem is referenced by:  coeq12d  5488  fcof1oinvd  6768  domss2  8354  mapen  8359  mapfien  8548  hashfacen  13451  relexpsucnnr  13984  relexpsucr  13988  relexpsucnnl  13991  relexpaddnn  14010  imasval  16372  cofuass  16749  cofulid  16750  setcinv  16940  catcisolem  16956  catciso  16957  yonedalem3b  17120  gsumvalx  17471  frmdup3lem  17604  symggrp  18017  f1omvdco2  18065  symggen  18087  psgnunilem1  18110  gsumval3  18505  gsumzf1o  18510  psrass1lem  19582  coe1add  19838  evls1fval  19888  evl1sca  19902  evl1var  19904  evls1var  19906  pf1mpf  19920  pf1ind  19923  znval  20087  znle2  20105  tchds  23239  dvnfval  23898  hocsubdir  28971  fcoinver  29742  fcobij  29826  symgfcoeu  30169  reprpmtf1o  31028  hgt750lemg  31056  subfacp1lem5  31487  mrsubffval  31725  mrsubfval  31726  mrsubrn  31731  elmrsubrn  31738  upixp  33834  ltrncoidN  35906  trlcoat  36501  trlcone  36506  cdlemg47a  36512  cdlemg47  36514  ltrnco4  36517  tendovalco  36543  tendoplcbv  36553  tendopl  36554  tendoplass  36561  tendo0pl  36569  tendoipl  36575  cdlemk45  36725  cdlemk53b  36734  cdlemk55a  36737  erngdvlem3  36768  erngdvlem3-rN  36776  tendocnv  36799  dvhvaddcbv  36867  dvhvaddval  36868  dvhvaddass  36875  dicvscacl  36969  cdlemn8  36982  dihordlem7b  36993  dihopelvalcpre  37026  relexp2  38466  relexpxpnnidm  38492  relexpiidm  38493  relexpmulnn  38498  relexpaddss  38507  trclfvcom  38512  trclfvdecomr  38517  frege131d  38553  dssmap2d  38813