Theorem coeq12d 5762

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

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-co 5589

This theorem is referenced by:  relcnvtrg  6159  xpcoid  6182  csbcog  6189  dfac12lem1  9830  dfac12r  9833  trcleq2lem  14630  trclfvcotrg  14655  relexpaddg  14692  relexpaddd  14693  dfrtrcl2  14701  imasval  17139  cofuval  17513  cofu2nd  17516  cofuval2  17518  cofuass  17520  cofurid  17522  setcco  17714  estrcco  17762  funcestrcsetclem9  17781  funcsetcestrclem9  17796  isdir  18231  smndex1mgm  18461  symgov  18906  znval  20651  znle2  20673  evl1fval  21404  mdetfval  21643  mdetdiaglem  21655  ust0  23279  trust  23289  metustexhalf  23618  isngp  23658  ngppropd  23699  tngval  23701  tngngp2  23722  imsval  28948  opsqrlem3  30405  hmopidmch  30416  hmopidmpj  30417  pjidmco  30444  dfpjop  30445  cosnop  30930  tocycfv  31278  cycpm2tr  31288  cyc3genpmlem  31320  cycpmconjslem2  31324  cycpmconjs  31325  cyc3conja  31326  zhmnrg  31817  bj-imdirco  35288  dftrrels2  36616  dftrrel2  36618  istendo  38701  tendoco2  38709  tendoidcl  38710  tendococl  38713  tendoplcbv  38716  tendopl2  38718  tendoplco2  38720  tendodi1  38725  tendodi2  38726  tendo0co2  38729  tendoicl  38737  erngplus2  38745  erngplus2-rN  38753  cdlemk55u1  38906  cdlemk55u  38907  dvaplusgv  38951  dvhopvadd  39034  dvhlveclem  39049  dvhopaddN  39055  dicvaddcl  39131  dihopelvalcpre  39189  rtrclex  41114  trclubgNEW  41115  rtrclexi  41118  cnvtrcl0  41123  dfrtrcl5  41126  trcleq2lemRP  41127  trrelind  41162  trrelsuperreldg  41165  trficl  41166  trrelsuperrel2dg  41168  trclrelexplem  41208  relexpaddss  41215  dfrtrcl3  41230  clsneicnv  41604  neicvgnvo  41614  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjALT  44752  rngccoALTV  45434  funcrngcsetcALT  45445  funcringcsetcALTV2lem9  45490  ringccoALTV  45497  funcringcsetclem9ALTV  45513