Theorem coeq12d 5813

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

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

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 3907  df-br 5087  df-opab 5149  df-co 5633

This theorem is referenced by:  relcnvtrg  6225  xpcoid  6248  csbcog  6255  dfac12lem1  10057  dfac12r  10060  trcleq2lem  14944  trclfvcotrg  14969  relexpaddg  15006  relexpaddd  15007  dfrtrcl2  15015  imasval  17466  cofuval  17840  cofu2nd  17843  cofuval2  17845  cofuass  17847  cofurid  17849  setcco  18041  estrcco  18087  funcestrcsetclem9  18105  funcsetcestrclem9  18120  isdir  18555  smndex1mgm  18869  symgov  19350  funcrngcsetcALT  20609  znval  21525  znle2  21543  evl1fval  22303  mdetfval  22561  mdetdiaglem  22573  ust0  24195  trust  24204  metustexhalf  24531  isngp  24571  ngppropd  24612  tngval  24614  tngngp2  24627  imsval  30771  opsqrlem3  32228  hmopidmch  32239  hmopidmpj  32240  pjidmco  32267  dfpjop  32268  cosnop  32783  tocycfv  33185  cycpm2tr  33195  cyc3genpmlem  33227  cycpmconjslem2  33231  cycpmconjs  33232  cyc3conja  33233  esplyval  33721  zhmnrg  34125  bj-imdirco  37520  dftrrels2  38994  dftrrel2  38996  istendo  41220  tendoco2  41228  tendoidcl  41229  tendococl  41232  tendoplcbv  41235  tendopl2  41237  tendoplco2  41239  tendodi1  41244  tendodi2  41245  tendo0co2  41248  tendoicl  41256  erngplus2  41264  erngplus2-rN  41272  cdlemk55u1  41425  cdlemk55u  41426  dvaplusgv  41470  dvhopvadd  41553  dvhlveclem  41568  dvhopaddN  41574  dicvaddcl  41650  dihopelvalcpre  41708  rtrclex  44062  trclubgNEW  44063  rtrclexi  44066  cnvtrcl0  44071  dfrtrcl5  44074  trcleq2lemRP  44075  trrelind  44110  trrelsuperreldg  44113  trficl  44114  trrelsuperrel2dg  44116  trclrelexplem  44156  relexpaddss  44163  dfrtrcl3  44178  clsneicnv  44550  neicvgnvo  44560  fundcmpsurbijinjpreimafv  47879  fundcmpsurinjALT  47884  rngccoALTV  48759  funcringcsetcALTV2lem9  48786  ringccoALTV  48793  funcringcsetclem9ALTV  48809  fuco112x  49819  fuco22natlem  49832  fucoppcid  49895