Theorem coeq12d 5834

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

Syntax hints:   → wi 4   = wceq 1559   ∘ ccom 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3921  df-br 5100  df-opab 5162  df-co 5654

This theorem is referenced by:  relcnvtrg  6250  xpcoid  6273  csbcog  6280  dfac12lem1  10097  dfac12r  10100  trcleq2lem  15001  trclfvcotrg  15026  relexpaddg  15063  relexpaddd  15064  dfrtrcl2  15072  imasval  17524  cofuval  17898  cofu2nd  17901  cofuval2  17903  cofuass  17905  cofurid  17907  setcco  18099  estrcco  18145  funcestrcsetclem9  18163  funcsetcestrclem9  18178  isdir  18613  smndex1mgm  18927  symgov  19407  funcrngcsetcALT  20670  znval  21567  znle2  21585  evl1fval  22371  mdetfval  22626  mdetdiaglem  22638  ust0  24260  trust  24269  metustexhalf  24596  isngp  24636  ngppropd  24677  tngval  24679  tngngp2  24692  imsval  30834  opsqrlem3  32291  hmopidmch  32302  hmopidmpj  32303  pjidmco  32330  dfpjop  32331  cosnop  32847  tocycfv  33250  cycpm2tr  33260  cyc3genpmlem  33292  cycpmconjslem2  33296  cycpmconjs  33297  cyc3conja  33298  esplyval  33820  zhmnrg  34223  bj-imdirco  37646  dftrrels2  39122  dftrrel2  39124  istendo  41348  tendoco2  41356  tendoidcl  41357  tendococl  41360  tendoplcbv  41363  tendopl2  41365  tendoplco2  41367  tendodi1  41372  tendodi2  41373  tendo0co2  41376  tendoicl  41384  erngplus2  41392  erngplus2-rN  41400  cdlemk55u1  41553  cdlemk55u  41554  dvaplusgv  41598  dvhopvadd  41681  dvhlveclem  41696  dvhopaddN  41702  dicvaddcl  41778  dihopelvalcpre  41836  rtrclex  44157  trclubgNEW  44158  rtrclexi  44161  cnvtrcl0  44166  dfrtrcl5  44169  trcleq2lemRP  44170  trrelind  44205  trrelsuperreldg  44208  trficl  44209  trrelsuperrel2dg  44211  trclrelexplem  44251  relexpaddss  44258  dfrtrcl3  44273  clsneicnv  44645  neicvgnvo  44655  fundcmpsurbijinjpreimafv  47977  fundcmpsurinjALT  47982  rngccoALTV  48857  funcringcsetcALTV2lem9  48884  ringccoALTV  48891  funcringcsetclem9ALTV  48907  fuco112x  49917  fuco22natlem  49930  fucoppcid  49993