Theorem coeq12d 5852

Description: Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)

Hypotheses

Ref	Expression
coeq12d.1	⊢ (𝜑 → 𝐴 = 𝐵)
coeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
coeq12d	⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))

Proof of Theorem coeq12d

Step	Hyp	Ref	Expression
1		coeq12d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	coeq1d 5849	. 2 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3		coeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	coeq2d 5850	. 2 ⊢ (𝜑 → (𝐵 ∘ 𝐶) = (𝐵 ∘ 𝐷))
5	2, 4	eqtrd 2798	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))

Syntax hints:   → wi 4   = wceq 1570   ∘ ccom 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3923  df-br 5111  df-opab 5175  df-co 5672

This theorem is referenced by:  relcnvtrg  6270  xpcoid  6293  csbcog  6300  dfac12lem1  10128  dfac12r  10131  trcleq2lem  15030  trclfvcotrg  15055  relexpaddg  15092  relexpaddd  15093  dfrtrcl2  15101  imasval  17566  cofuval  17940  cofu2nd  17943  cofuval2  17945  cofuass  17947  cofurid  17949  setcco  18141  estrcco  18187  funcestrcsetclem9  18205  funcsetcestrclem9  18220  isdir  18655  smndex1mgm  18970  symgov  19455  funcrngcsetcALT  20727  znval  21666  znle2  21684  evl1fval  22469  mdetfval  22724  mdetdiaglem  22736  ust0  24358  trust  24367  metustexhalf  24694  isngp  24734  ngppropd  24775  tngval  24777  tngngp2  24790  imsval  31015  opsqrlem3  32472  hmopidmch  32483  hmopidmpj  32484  pjidmco  32511  dfpjop  32512  cosnop  33018  tocycfv  33407  cycpm2tr  33417  cyc3genpmlem  33449  cycpmconjslem2  33453  cycpmconjs  33454  cyc3conja  33455  esplyval  33930  zhmnrg  34333  bj-imdirco  37812  dftrrels2  39286  dftrrel2  39288  istendo  41512  tendoco2  41520  tendoidcl  41521  tendococl  41524  tendoplcbv  41527  tendopl2  41529  tendoplco2  41531  tendodi1  41536  tendodi2  41537  tendo0co2  41540  tendoicl  41548  erngplus2  41556  erngplus2-rN  41564  cdlemk55u1  41717  cdlemk55u  41718  dvaplusgv  41762  dvhopvadd  41845  dvhlveclem  41860  dvhopaddN  41866  dicvaddcl  41942  dihopelvalcpre  42000  rtrclex  44323  trclubgNEW  44324  rtrclexi  44327  cnvtrcl0  44332  dfrtrcl5  44335  trcleq2lemRP  44336  trrelind  44371  trrelsuperreldg  44374  trficl  44375  trrelsuperrel2dg  44377  trclrelexplem  44417  relexpaddss  44424  dfrtrcl3  44439  clsneicnv  44811  neicvgnvo  44821  fundcmpsurbijinjpreimafv  48133  fundcmpsurinjALT  48138  rngccoALTV  49013  funcringcsetcALTV2lem9  49040  ringccoALTV  49047  funcringcsetclem9ALTV  49063  fuco112x  50087  fuco22natlem  50100  fucoppcid  50163