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  29969  opsqrlem3  31426  hmopidmch  31437  hmopidmpj  31438  pjidmco  31465  dfpjop  31466  cosnop  31948  tocycfv  32299  cycpm2tr  32309  cyc3genpmlem  32341  cycpmconjslem2  32345  cycpmconjs  32346  cyc3conja  32347  zhmnrg  32978  bj-imdirco  36119  dftrrels2  37493  dftrrel2  37495  istendo  39679  tendoco2  39687  tendoidcl  39688  tendococl  39691  tendoplcbv  39694  tendopl2  39696  tendoplco2  39698  tendodi1  39703  tendodi2  39704  tendo0co2  39707  tendoicl  39715  erngplus2  39723  erngplus2-rN  39731  cdlemk55u1  39884  cdlemk55u  39885  dvaplusgv  39929  dvhopvadd  40012  dvhlveclem  40027  dvhopaddN  40033  dicvaddcl  40109  dihopelvalcpre  40167  rtrclex  42416  trclubgNEW  42417  rtrclexi  42420  cnvtrcl0  42425  dfrtrcl5  42428  trcleq2lemRP  42429  trrelind  42464  trrelsuperreldg  42467  trficl  42468  trrelsuperrel2dg  42470  trclrelexplem  42510  relexpaddss  42517  dfrtrcl3  42532  clsneicnv  42904  neicvgnvo  42914  fundcmpsurbijinjpreimafv  46123  fundcmpsurinjALT  46128  rngccoALTV  46934  funcrngcsetcALT  46945  funcringcsetcALTV2lem9  46990  ringccoALTV  46997  funcringcsetclem9ALTV  47013