Theorem coeq1d 5734

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

Syntax hints:   → wi 4   = wceq 1537   ∘ ccom 5561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954  df-br 5069  df-opab 5131  df-co 5566

This theorem is referenced by:  coeq12d  5737  fcof1oinvd  7051  domss2  8678  mapen  8683  mapfien  8873  hashfacen  13815  relexpsucnnr  14386  relexpsucr  14390  relexpsucnnl  14393  relexpaddnn  14412  imasval  16786  cofuass  17161  cofulid  17162  setcinv  17352  catcisolem  17368  catciso  17369  yonedalem3b  17531  gsumvalx  17888  frmdup3lem  18033  symggrplem  18051  f1omvdco2  18578  symggen  18600  psgnunilem1  18623  gsumval3  19029  gsumzf1o  19034  psrass1lem  20159  coe1add  20434  evls1fval  20484  evl1sca  20499  evl1var  20501  evls1var  20503  pf1mpf  20517  pf1ind  20520  znval  20684  znle2  20702  tcphds  23836  dvnfval  24521  hocsubdir  29564  fcoinver  30359  fcobij  30460  symgfcoeu  30728  symgcom  30729  pmtrcnel2  30736  tocyc01  30762  cycpm2tr  30763  cycpmconjv  30786  cycpmconjslem1  30798  cycpmconjslem2  30799  cycpmconjs  30800  cyc3conja  30801  reprpmtf1o  31899  hgt750lemg  31927  subfacp1lem5  32433  mrsubffval  32756  mrsubfval  32757  mrsubrn  32762  elmrsubrn  32769  upixp  35006  ltrncoidN  37266  trlcoat  37861  trlcone  37866  cdlemg47a  37872  cdlemg47  37874  ltrnco4  37877  tendovalco  37903  tendoplcbv  37913  tendopl  37914  tendoplass  37921  tendo0pl  37929  tendoipl  37935  cdlemk45  38085  cdlemk53b  38094  cdlemk55a  38097  erngdvlem3  38128  erngdvlem3-rN  38136  tendocnv  38159  dvhvaddcbv  38227  dvhvaddval  38228  dvhvaddass  38235  dicvscacl  38329  cdlemn8  38342  dihordlem7b  38353  dihopelvalcpre  38386  relexp2  40029  relexpxpnnidm  40055  relexpiidm  40056  relexpmulnn  40061  relexpaddss  40070  trclfvcom  40075  trclfvdecomr  40080  frege131d  40116  dssmap2d  40375  fundcmpsurbijinjpreimafv  43574  isomushgr  43998