Theorem coeq1d 4999

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
coeq1d	|- ( ph -> ( A o. C ) = ( B o. C ) )

Proof of Theorem coeq1d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 |- ( ph -> A = B )
2		coeq1 4995	. 2 |- ( A = B -> ( A o. C ) = ( B o. C ) )
3	1, 2	syl 17	1 |- ( ph -> ( A o. C ) = ( B o. C ) )

Syntax hints:   -> wi 4   = wceq 1446   o. ccom 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-in 3413  df-ss 3420  df-br 4406  df-opab 4465  df-co 4846

This theorem is referenced by:  coeq12d  5002  fcof1oinvd  6196  domss2  7736  mapen  7741  mapfien  7926  hashfacen  12624  relexpsucnnr  13100  relexpsucr  13104  relexpsucnnl  13107  relexpaddnn  13126  imasval  15423  imasvalOLD  15424  cofuass  15806  cofulid  15807  setcinv  15997  catcisolem  16013  catciso  16014  yonedalem3b  16176  gsumvalx  16525  frmdup3lem  16662  symggrp  17053  f1omvdco2  17101  symggen  17123  psgnunilem1  17146  gsumval3  17553  gsumzf1o  17558  psrass1lem  18613  coe1add  18869  evls1fval  18920  evl1sca  18934  evl1var  18936  evls1var  18938  pf1mpf  18952  pf1ind  18955  znval  19118  znle2  19136  tchds  22217  dvnfval  22888  hocsubdir  27450  fcoinver  28226  fcobij  28322  symgfcoeu  28620  subfacp1lem5  29919  mrsubffval  30157  mrsubfval  30158  mrsubrn  30163  elmrsubrn  30170  upixp  32068  ltrncoidN  33705  trlcoat  34302  trlcone  34307  cdlemg47a  34313  cdlemg47  34315  ltrnco4  34318  tendovalco  34344  tendoplcbv  34354  tendopl  34355  tendoplass  34362  tendo0pl  34370  tendoipl  34376  cdlemk45  34526  cdlemk53b  34535  cdlemk55a  34538  erngdvlem3  34569  erngdvlem3-rN  34577  tendocnv  34601  dvhvaddcbv  34669  dvhvaddval  34670  dvhvaddass  34677  dicvscacl  34771  cdlemn8  34784  dihordlem7b  34795  dihopelvalcpre  34828  relexp2  36281  relexpxpnnidm  36307  relexpiidm  36308  relexpmulnn  36313  relexpaddss  36322  trclfvcom  36327  trclfvdecomr  36332  frege131d  36368