Theorem coeq12d 5865

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 5862	. 2 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3		coeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	coeq2d 5863	. 2 ⊢ (𝜑 → (𝐵 ∘ 𝐶) = (𝐵 ∘ 𝐷))
5	2, 4	eqtrd 2773	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686

This theorem is referenced by:  relcnvtrg  6266  xpcoid  6290  csbcog  6297  dfac12lem1  10138  dfac12r  10141  trcleq2lem  14938  trclfvcotrg  14963  relexpaddg  15000  relexpaddd  15001  dfrtrcl2  15009  imasval  17457  cofuval  17832  cofu2nd  17835  cofuval2  17837  cofuass  17839  cofurid  17841  setcco  18033  estrcco  18081  funcestrcsetclem9  18100  funcsetcestrclem9  18115  isdir  18551  smndex1mgm  18788  symgov  19251  znval  21087  znle2  21109  evl1fval  21847  mdetfval  22088  mdetdiaglem  22100  ust0  23724  trust  23734  metustexhalf  24065  isngp  24105  ngppropd  24146  tngval  24148  tngngp2  24169  imsval  29938  opsqrlem3  31395  hmopidmch  31406  hmopidmpj  31407  pjidmco  31434  dfpjop  31435  cosnop  31917  tocycfv  32268  cycpm2tr  32278  cyc3genpmlem  32310  cycpmconjslem2  32314  cycpmconjs  32315  cyc3conja  32316  zhmnrg  32947  bj-imdirco  36071  dftrrels2  37445  dftrrel2  37447  istendo  39631  tendoco2  39639  tendoidcl  39640  tendococl  39643  tendoplcbv  39646  tendopl2  39648  tendoplco2  39650  tendodi1  39655  tendodi2  39656  tendo0co2  39659  tendoicl  39667  erngplus2  39675  erngplus2-rN  39683  cdlemk55u1  39836  cdlemk55u  39837  dvaplusgv  39881  dvhopvadd  39964  dvhlveclem  39979  dvhopaddN  39985  dicvaddcl  40061  dihopelvalcpre  40119  rtrclex  42368  trclubgNEW  42369  rtrclexi  42372  cnvtrcl0  42377  dfrtrcl5  42380  trcleq2lemRP  42381  trrelind  42416  trrelsuperreldg  42419  trficl  42420  trrelsuperrel2dg  42422  trclrelexplem  42462  relexpaddss  42469  dfrtrcl3  42484  clsneicnv  42856  neicvgnvo  42866  fundcmpsurbijinjpreimafv  46075  fundcmpsurinjALT  46080  rngccoALTV  46886  funcrngcsetcALT  46897  funcringcsetcALTV2lem9  46942  ringccoALTV  46949  funcringcsetclem9ALTV  46965