Theorem coeq1d 5808

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

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

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 3922  df-br 5096  df-opab 5158  df-co 5632

This theorem is referenced by:  coeq12d  5811  fcof1oinvd  7234  domss2  9060  mapen  9065  mapfien  9317  hashfacen  14380  relexpsucnnr  14951  relexpsucnnl  14956  relexpsucr  14958  relexpsucrd  14959  relexpaddnn  14977  imasval  17434  cofuass  17815  cofulid  17816  setcinv  18016  catcisolem  18036  catciso  18037  yonedalem3b  18204  gsumvalx  18569  frmdup3lem  18759  symggrplem  18777  f1omvdco2  19346  symggen  19368  psgnunilem1  19391  gsumval3  19805  gsumzf1o  19810  znval  21461  znle2  21479  psrass1lem  21858  coe1add  22167  evls1fval  22223  evl1sca  22238  evl1var  22240  evls1var  22242  pf1mpf  22256  pf1ind  22259  tcphds  25148  dvnfval  25841  hocsubdir  31748  fcoinver  32567  fcobij  32683  ccatws1f1olast  32913  symgfcoeu  33043  symgcom  33044  pmtrcnel2  33051  tocyc01  33079  cycpm2tr  33080  cycpmconjv  33103  cycpmconjslem1  33115  cycpmconjslem2  33116  cycpmconjs  33117  cyc3conja  33118  1arithidomlem2  33492  mplvrpmga  33565  reprpmtf1o  34613  hgt750lemg  34641  subfacp1lem5  35176  mrsubffval  35499  mrsubfval  35500  mrsubrn  35505  elmrsubrn  35512  upixp  37728  ltrncoidN  40127  trlcoat  40722  trlcone  40727  cdlemg47a  40733  cdlemg47  40735  ltrnco4  40738  tendovalco  40764  tendoplcbv  40774  tendopl  40775  tendoplass  40782  tendo0pl  40790  tendoipl  40796  cdlemk45  40946  cdlemk53b  40955  cdlemk55a  40958  erngdvlem3  40989  erngdvlem3-rN  40997  tendocnv  41020  dvhvaddcbv  41088  dvhvaddval  41089  dvhvaddass  41096  dicvscacl  41190  cdlemn8  41203  dihordlem7b  41214  dihopelvalcpre  41247  aks6d1c6lem5  42170  relexp2  43670  relexpxpnnidm  43696  relexpiidm  43697  relexpmulnn  43702  relexpaddss  43711  trclfvcom  43716  trclfvdecomr  43721  frege131d  43757  dssmap2d  44015  fundcmpsurbijinjpreimafv  47411  gricushgr  47921  prcof21a  49396