Theorem coeq1d 5283

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

Syntax hints:   → wi 4   = wceq 1483   ∘ ccom 5118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-co 5123

This theorem is referenced by:  coeq12d  5286  fcof1oinvd  6548  domss2  8119  mapen  8124  mapfien  8313  hashfacen  13238  relexpsucnnr  13765  relexpsucr  13769  relexpsucnnl  13772  relexpaddnn  13791  imasval  16171  cofuass  16549  cofulid  16550  setcinv  16740  catcisolem  16756  catciso  16757  yonedalem3b  16919  gsumvalx  17270  frmdup3lem  17403  symggrp  17820  f1omvdco2  17868  symggen  17890  psgnunilem1  17913  gsumval3  18308  gsumzf1o  18313  psrass1lem  19377  coe1add  19634  evls1fval  19684  evl1sca  19698  evl1var  19700  evls1var  19702  pf1mpf  19716  pf1ind  19719  znval  19883  znle2  19902  tchds  23030  dvnfval  23685  hocsubdir  28644  fcoinver  29418  fcobij  29500  symgfcoeu  29845  reprpmtf1o  30704  hgt750lemg  30732  subfacp1lem5  31166  mrsubffval  31404  mrsubfval  31405  mrsubrn  31410  elmrsubrn  31417  upixp  33524  ltrncoidN  35414  trlcoat  36011  trlcone  36016  cdlemg47a  36022  cdlemg47  36024  ltrnco4  36027  tendovalco  36053  tendoplcbv  36063  tendopl  36064  tendoplass  36071  tendo0pl  36079  tendoipl  36085  cdlemk45  36235  cdlemk53b  36244  cdlemk55a  36247  erngdvlem3  36278  erngdvlem3-rN  36286  tendocnv  36310  dvhvaddcbv  36378  dvhvaddval  36379  dvhvaddass  36386  dicvscacl  36480  cdlemn8  36493  dihordlem7b  36504  dihopelvalcpre  36537  relexp2  37969  relexpxpnnidm  37995  relexpiidm  37996  relexpmulnn  38001  relexpaddss  38010  trclfvcom  38015  trclfvdecomr  38020  frege131d  38056  dssmap2d  38316