Theorem coeq12d 5889

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

Syntax hints:   → wi 4   = wceq 1537   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  relcnvtrg  6297  xpcoid  6321  csbcog  6328  dfac12lem1  10213  dfac12r  10216  trcleq2lem  15040  trclfvcotrg  15065  relexpaddg  15102  relexpaddd  15103  dfrtrcl2  15111  imasval  17571  cofuval  17946  cofu2nd  17949  cofuval2  17951  cofuass  17953  cofurid  17955  setcco  18150  estrcco  18198  funcestrcsetclem9  18217  funcsetcestrclem9  18232  isdir  18668  smndex1mgm  18942  symgov  19425  funcrngcsetcALT  20663  znval  21573  znle2  21595  evl1fval  22353  mdetfval  22613  mdetdiaglem  22625  ust0  24249  trust  24259  metustexhalf  24590  isngp  24630  ngppropd  24671  tngval  24673  tngngp2  24694  imsval  30717  opsqrlem3  32174  hmopidmch  32185  hmopidmpj  32186  pjidmco  32213  dfpjop  32214  cosnop  32707  tocycfv  33102  cycpm2tr  33112  cyc3genpmlem  33144  cycpmconjslem2  33148  cycpmconjs  33149  cyc3conja  33150  zhmnrg  33913  bj-imdirco  37156  dftrrels2  38531  dftrrel2  38533  istendo  40717  tendoco2  40725  tendoidcl  40726  tendococl  40729  tendoplcbv  40732  tendopl2  40734  tendoplco2  40736  tendodi1  40741  tendodi2  40742  tendo0co2  40745  tendoicl  40753  erngplus2  40761  erngplus2-rN  40769  cdlemk55u1  40922  cdlemk55u  40923  dvaplusgv  40967  dvhopvadd  41050  dvhlveclem  41065  dvhopaddN  41071  dicvaddcl  41147  dihopelvalcpre  41205  rtrclex  43579  trclubgNEW  43580  rtrclexi  43583  cnvtrcl0  43588  dfrtrcl5  43591  trcleq2lemRP  43592  trrelind  43627  trrelsuperreldg  43630  trficl  43631  trrelsuperrel2dg  43633  trclrelexplem  43673  relexpaddss  43680  dfrtrcl3  43695  clsneicnv  44067  neicvgnvo  44077  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjALT  47286  rngccoALTV  47994  funcringcsetcALTV2lem9  48021  ringccoALTV  48028  funcringcsetclem9ALTV  48044