Theorem coeq12d 5875

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694

This theorem is referenced by:  relcnvtrg  6286  xpcoid  6310  csbcog  6317  dfac12lem1  10184  dfac12r  10187  trcleq2lem  15030  trclfvcotrg  15055  relexpaddg  15092  relexpaddd  15093  dfrtrcl2  15101  imasval  17556  cofuval  17927  cofu2nd  17930  cofuval2  17932  cofuass  17934  cofurid  17936  setcco  18128  estrcco  18174  funcestrcsetclem9  18193  funcsetcestrclem9  18208  isdir  18643  smndex1mgm  18920  symgov  19401  funcrngcsetcALT  20641  znval  21550  znle2  21572  evl1fval  22332  mdetfval  22592  mdetdiaglem  22604  ust0  24228  trust  24238  metustexhalf  24569  isngp  24609  ngppropd  24650  tngval  24652  tngngp2  24673  imsval  30704  opsqrlem3  32161  hmopidmch  32172  hmopidmpj  32173  pjidmco  32200  dfpjop  32201  cosnop  32704  tocycfv  33129  cycpm2tr  33139  cyc3genpmlem  33171  cycpmconjslem2  33175  cycpmconjs  33176  cyc3conja  33177  zhmnrg  33966  bj-imdirco  37191  dftrrels2  38576  dftrrel2  38578  istendo  40762  tendoco2  40770  tendoidcl  40771  tendococl  40774  tendoplcbv  40777  tendopl2  40779  tendoplco2  40781  tendodi1  40786  tendodi2  40787  tendo0co2  40790  tendoicl  40798  erngplus2  40806  erngplus2-rN  40814  cdlemk55u1  40967  cdlemk55u  40968  dvaplusgv  41012  dvhopvadd  41095  dvhlveclem  41110  dvhopaddN  41116  dicvaddcl  41192  dihopelvalcpre  41250  rtrclex  43630  trclubgNEW  43631  rtrclexi  43634  cnvtrcl0  43639  dfrtrcl5  43642  trcleq2lemRP  43643  trrelind  43678  trrelsuperreldg  43681  trficl  43682  trrelsuperrel2dg  43684  trclrelexplem  43724  relexpaddss  43731  dfrtrcl3  43746  clsneicnv  44118  neicvgnvo  44128  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjALT  47399  rngccoALTV  48187  funcringcsetcALTV2lem9  48214  ringccoALTV  48221  funcringcsetclem9ALTV  48237  fuco112x  49027  fuco22natlem  49040