Theorem coeq1d 5872

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

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5689

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694

This theorem is referenced by:  coeq12d  5875  fcof1oinvd  7313  domss2  9176  mapen  9181  mapfien  9448  hashfacen  14493  relexpsucnnr  15064  relexpsucnnl  15069  relexpsucr  15071  relexpsucrd  15072  relexpaddnn  15090  imasval  17556  cofuass  17934  cofulid  17935  setcinv  18135  catcisolem  18155  catciso  18156  yonedalem3b  18324  gsumvalx  18689  frmdup3lem  18879  symggrplem  18897  f1omvdco2  19466  symggen  19488  psgnunilem1  19511  gsumval3  19925  gsumzf1o  19930  znval  21550  znle2  21572  psrass1lem  21952  coe1add  22267  evls1fval  22323  evl1sca  22338  evl1var  22340  evls1var  22342  pf1mpf  22356  pf1ind  22359  tcphds  25265  dvnfval  25958  hocsubdir  31804  fcoinver  32617  fcobij  32733  ccatws1f1olast  32937  symgfcoeu  33102  symgcom  33103  pmtrcnel2  33110  tocyc01  33138  cycpm2tr  33139  cycpmconjv  33162  cycpmconjslem1  33174  cycpmconjslem2  33175  cycpmconjs  33176  cyc3conja  33177  1arithidomlem2  33564  reprpmtf1o  34641  hgt750lemg  34669  subfacp1lem5  35189  mrsubffval  35512  mrsubfval  35513  mrsubrn  35518  elmrsubrn  35525  upixp  37736  ltrncoidN  40130  trlcoat  40725  trlcone  40730  cdlemg47a  40736  cdlemg47  40738  ltrnco4  40741  tendovalco  40767  tendoplcbv  40777  tendopl  40778  tendoplass  40785  tendo0pl  40793  tendoipl  40799  cdlemk45  40949  cdlemk53b  40958  cdlemk55a  40961  erngdvlem3  40992  erngdvlem3-rN  41000  tendocnv  41023  dvhvaddcbv  41091  dvhvaddval  41092  dvhvaddass  41099  dicvscacl  41193  cdlemn8  41206  dihordlem7b  41217  dihopelvalcpre  41250  aks6d1c6lem5  42178  relexp2  43690  relexpxpnnidm  43716  relexpiidm  43717  relexpmulnn  43722  relexpaddss  43731  trclfvcom  43736  trclfvdecomr  43741  frege131d  43777  dssmap2d  44035  fundcmpsurbijinjpreimafv  47394  gricushgr  47886