Theorem coeq12d 5844

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-co 5663

This theorem is referenced by:  relcnvtrg  6255  xpcoid  6279  csbcog  6286  dfac12lem1  10156  dfac12r  10159  trcleq2lem  15008  trclfvcotrg  15033  relexpaddg  15070  relexpaddd  15071  dfrtrcl2  15079  imasval  17523  cofuval  17893  cofu2nd  17896  cofuval2  17898  cofuass  17900  cofurid  17902  setcco  18094  estrcco  18140  funcestrcsetclem9  18158  funcsetcestrclem9  18173  isdir  18606  smndex1mgm  18883  symgov  19363  funcrngcsetcALT  20599  znval  21494  znle2  21512  evl1fval  22264  mdetfval  22522  mdetdiaglem  22534  ust0  24156  trust  24166  metustexhalf  24493  isngp  24533  ngppropd  24574  tngval  24576  tngngp2  24589  imsval  30612  opsqrlem3  32069  hmopidmch  32080  hmopidmpj  32081  pjidmco  32108  dfpjop  32109  cosnop  32618  tocycfv  33066  cycpm2tr  33076  cyc3genpmlem  33108  cycpmconjslem2  33112  cycpmconjs  33113  cyc3conja  33114  zhmnrg  33942  bj-imdirco  37154  dftrrels2  38539  dftrrel2  38541  istendo  40725  tendoco2  40733  tendoidcl  40734  tendococl  40737  tendoplcbv  40740  tendopl2  40742  tendoplco2  40744  tendodi1  40749  tendodi2  40750  tendo0co2  40753  tendoicl  40761  erngplus2  40769  erngplus2-rN  40777  cdlemk55u1  40930  cdlemk55u  40931  dvaplusgv  40975  dvhopvadd  41058  dvhlveclem  41073  dvhopaddN  41079  dicvaddcl  41155  dihopelvalcpre  41213  rtrclex  43588  trclubgNEW  43589  rtrclexi  43592  cnvtrcl0  43597  dfrtrcl5  43600  trcleq2lemRP  43601  trrelind  43636  trrelsuperreldg  43639  trficl  43640  trrelsuperrel2dg  43642  trclrelexplem  43682  relexpaddss  43689  dfrtrcl3  43704  clsneicnv  44076  neicvgnvo  44086  fundcmpsurbijinjpreimafv  47369  fundcmpsurinjALT  47374  rngccoALTV  48194  funcringcsetcALTV2lem9  48221  ringccoALTV  48228  funcringcsetclem9ALTV  48244  fuco112x  49191  fuco22natlem  49204