Theorem coeq1d 5205

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

Syntax hints:   → wi 4   = wceq 1475   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-co 5047

This theorem is referenced by:  coeq12d  5208  fcof1oinvd  6448  domss2  8004  mapen  8009  mapfien  8196  hashfacen  13095  relexpsucnnr  13613  relexpsucr  13617  relexpsucnnl  13620  relexpaddnn  13639  imasval  15994  cofuass  16372  cofulid  16373  setcinv  16563  catcisolem  16579  catciso  16580  yonedalem3b  16742  gsumvalx  17093  frmdup3lem  17226  symggrp  17643  f1omvdco2  17691  symggen  17713  psgnunilem1  17736  gsumval3  18131  gsumzf1o  18136  psrass1lem  19198  coe1add  19455  evls1fval  19505  evl1sca  19519  evl1var  19521  evls1var  19523  pf1mpf  19537  pf1ind  19540  znval  19702  znle2  19721  tchds  22838  dvnfval  23491  hocsubdir  28028  fcoinver  28798  fcobij  28888  symgfcoeu  29176  subfacp1lem5  30420  mrsubffval  30658  mrsubfval  30659  mrsubrn  30664  elmrsubrn  30671  upixp  32694  ltrncoidN  34432  trlcoat  35029  trlcone  35034  cdlemg47a  35040  cdlemg47  35042  ltrnco4  35045  tendovalco  35071  tendoplcbv  35081  tendopl  35082  tendoplass  35089  tendo0pl  35097  tendoipl  35103  cdlemk45  35253  cdlemk53b  35262  cdlemk55a  35265  erngdvlem3  35296  erngdvlem3-rN  35304  tendocnv  35328  dvhvaddcbv  35396  dvhvaddval  35397  dvhvaddass  35404  dicvscacl  35498  cdlemn8  35511  dihordlem7b  35522  dihopelvalcpre  35555  relexp2  36988  relexpxpnnidm  37014  relexpiidm  37015  relexpmulnn  37020  relexpaddss  37029  trclfvcom  37034  trclfvdecomr  37039  frege131d  37075  dssmap2d  37336