Theorem coeq1d 5773

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

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-br 5076  df-opab 5138  df-co 5599

This theorem is referenced by:  coeq12d  5776  fcof1oinvd  7174  domss2  8932  mapen  8937  mapfien  9176  hashfacen  14175  hashfacenOLD  14176  relexpsucnnr  14745  relexpsucnnl  14750  relexpsucr  14752  relexpsucrd  14753  relexpaddnn  14771  imasval  17231  cofuass  17613  cofulid  17614  setcinv  17814  catcisolem  17834  catciso  17835  yonedalem3b  18006  gsumvalx  18369  frmdup3lem  18514  symggrplem  18532  f1omvdco2  19065  symggen  19087  psgnunilem1  19110  gsumval3  19517  gsumzf1o  19522  znval  20748  znle2  20770  psrass1lemOLD  21152  psrass1lem  21155  coe1add  21444  evls1fval  21494  evl1sca  21509  evl1var  21511  evls1var  21513  pf1mpf  21527  pf1ind  21530  tcphds  24404  dvnfval  25095  hocsubdir  30156  fcoinver  30955  fcobij  31066  symgfcoeu  31360  symgcom  31361  pmtrcnel2  31368  tocyc01  31394  cycpm2tr  31395  cycpmconjv  31418  cycpmconjslem1  31430  cycpmconjslem2  31431  cycpmconjs  31432  cyc3conja  31433  reprpmtf1o  32615  hgt750lemg  32643  subfacp1lem5  33155  mrsubffval  33478  mrsubfval  33479  mrsubrn  33484  elmrsubrn  33491  upixp  35896  ltrncoidN  38149  trlcoat  38744  trlcone  38749  cdlemg47a  38755  cdlemg47  38757  ltrnco4  38760  tendovalco  38786  tendoplcbv  38796  tendopl  38797  tendoplass  38804  tendo0pl  38812  tendoipl  38818  cdlemk45  38968  cdlemk53b  38977  cdlemk55a  38980  erngdvlem3  39011  erngdvlem3-rN  39019  tendocnv  39042  dvhvaddcbv  39110  dvhvaddval  39111  dvhvaddass  39118  dicvscacl  39212  cdlemn8  39225  dihordlem7b  39236  dihopelvalcpre  39269  relexp2  41292  relexpxpnnidm  41318  relexpiidm  41319  relexpmulnn  41324  relexpaddss  41333  trclfvcom  41338  trclfvdecomr  41343  frege131d  41379  dssmap2d  41637  fundcmpsurbijinjpreimafv  44870  isomushgr  45289