Theorem coeq12d 5831

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

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-co 5650

This theorem is referenced by:  relcnvtrg  6242  xpcoid  6266  csbcog  6273  dfac12lem1  10104  dfac12r  10107  trcleq2lem  14964  trclfvcotrg  14989  relexpaddg  15026  relexpaddd  15027  dfrtrcl2  15035  imasval  17481  cofuval  17851  cofu2nd  17854  cofuval2  17856  cofuass  17858  cofurid  17860  setcco  18052  estrcco  18098  funcestrcsetclem9  18116  funcsetcestrclem9  18131  isdir  18564  smndex1mgm  18841  symgov  19321  funcrngcsetcALT  20557  znval  21452  znle2  21470  evl1fval  22222  mdetfval  22480  mdetdiaglem  22492  ust0  24114  trust  24124  metustexhalf  24451  isngp  24491  ngppropd  24532  tngval  24534  tngngp2  24547  imsval  30621  opsqrlem3  32078  hmopidmch  32089  hmopidmpj  32090  pjidmco  32117  dfpjop  32118  cosnop  32625  tocycfv  33073  cycpm2tr  33083  cyc3genpmlem  33115  cycpmconjslem2  33119  cycpmconjs  33120  cyc3conja  33121  zhmnrg  33962  bj-imdirco  37185  dftrrels2  38573  dftrrel2  38575  istendo  40761  tendoco2  40769  tendoidcl  40770  tendococl  40773  tendoplcbv  40776  tendopl2  40778  tendoplco2  40780  tendodi1  40785  tendodi2  40786  tendo0co2  40789  tendoicl  40797  erngplus2  40805  erngplus2-rN  40813  cdlemk55u1  40966  cdlemk55u  40967  dvaplusgv  41011  dvhopvadd  41094  dvhlveclem  41109  dvhopaddN  41115  dicvaddcl  41191  dihopelvalcpre  41249  rtrclex  43613  trclubgNEW  43614  rtrclexi  43617  cnvtrcl0  43622  dfrtrcl5  43625  trcleq2lemRP  43626  trrelind  43661  trrelsuperreldg  43664  trficl  43665  trrelsuperrel2dg  43667  trclrelexplem  43707  relexpaddss  43714  dfrtrcl3  43729  clsneicnv  44101  neicvgnvo  44111  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjALT  47417  rngccoALTV  48263  funcringcsetcALTV2lem9  48290  ringccoALTV  48297  funcringcsetclem9ALTV  48313  fuco112x  49325  fuco22natlem  49338  fucoppcid  49401