Theorem coeq12d 5821

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-co 5641

This theorem is referenced by:  relcnvtrg  6233  xpcoid  6256  csbcog  6263  dfac12lem1  10066  dfac12r  10069  trcleq2lem  14926  trclfvcotrg  14951  relexpaddg  14988  relexpaddd  14989  dfrtrcl2  14997  imasval  17444  cofuval  17818  cofu2nd  17821  cofuval2  17823  cofuass  17825  cofurid  17827  setcco  18019  estrcco  18065  funcestrcsetclem9  18083  funcsetcestrclem9  18098  isdir  18533  smndex1mgm  18844  symgov  19325  funcrngcsetcALT  20586  znval  21502  znle2  21520  evl1fval  22284  mdetfval  22542  mdetdiaglem  22554  ust0  24176  trust  24185  metustexhalf  24512  isngp  24552  ngppropd  24593  tngval  24595  tngngp2  24608  imsval  30772  opsqrlem3  32229  hmopidmch  32240  hmopidmpj  32241  pjidmco  32268  dfpjop  32269  cosnop  32784  tocycfv  33202  cycpm2tr  33212  cyc3genpmlem  33244  cycpmconjslem2  33248  cycpmconjs  33249  cyc3conja  33250  esplyval  33738  zhmnrg  34142  bj-imdirco  37439  dftrrels2  38904  dftrrel2  38906  istendo  41130  tendoco2  41138  tendoidcl  41139  tendococl  41142  tendoplcbv  41145  tendopl2  41147  tendoplco2  41149  tendodi1  41154  tendodi2  41155  tendo0co2  41158  tendoicl  41166  erngplus2  41174  erngplus2-rN  41182  cdlemk55u1  41335  cdlemk55u  41336  dvaplusgv  41380  dvhopvadd  41463  dvhlveclem  41478  dvhopaddN  41484  dicvaddcl  41560  dihopelvalcpre  41618  rtrclex  43967  trclubgNEW  43968  rtrclexi  43971  cnvtrcl0  43976  dfrtrcl5  43979  trcleq2lemRP  43980  trrelind  44015  trrelsuperreldg  44018  trficl  44019  trrelsuperrel2dg  44021  trclrelexplem  44061  relexpaddss  44068  dfrtrcl3  44083  clsneicnv  44455  neicvgnvo  44465  fundcmpsurbijinjpreimafv  47761  fundcmpsurinjALT  47766  rngccoALTV  48625  funcringcsetcALTV2lem9  48652  ringccoALTV  48659  funcringcsetclem9ALTV  48675  fuco112x  49685  fuco22natlem  49698  fucoppcid  49761