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 2775	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷))

Syntax hints:   → wi 4   = wceq 1547   ∘ ccom 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-br 5080  df-opab 5142  df-co 5634

This theorem is referenced by:  relcnvtrg  6225  xpcoid  6248  csbcog  6255  dfac12lem1  10064  dfac12r  10067  trcleq2lem  14951  trclfvcotrg  14976  relexpaddg  15013  relexpaddd  15014  dfrtrcl2  15022  imasval  17473  cofuval  17847  cofu2nd  17850  cofuval2  17852  cofuass  17854  cofurid  17856  setcco  18048  estrcco  18094  funcestrcsetclem9  18112  funcsetcestrclem9  18127  isdir  18562  smndex1mgm  18876  symgov  19357  funcrngcsetcALT  20620  znval  21517  znle2  21535  evl1fval  22321  mdetfval  22576  mdetdiaglem  22588  ust0  24210  trust  24219  metustexhalf  24546  isngp  24586  ngppropd  24627  tngval  24629  tngngp2  24642  imsval  30781  opsqrlem3  32238  hmopidmch  32249  hmopidmpj  32250  pjidmco  32277  dfpjop  32278  cosnop  32794  tocycfv  33197  cycpm2tr  33207  cyc3genpmlem  33239  cycpmconjslem2  33243  cycpmconjs  33244  cyc3conja  33245  esplyval  33753  zhmnrg  34156  bj-imdirco  37557  dftrrels2  39033  dftrrel2  39035  istendo  41259  tendoco2  41267  tendoidcl  41268  tendococl  41271  tendoplcbv  41274  tendopl2  41276  tendoplco2  41278  tendodi1  41283  tendodi2  41284  tendo0co2  41287  tendoicl  41295  erngplus2  41303  erngplus2-rN  41311  cdlemk55u1  41464  cdlemk55u  41465  dvaplusgv  41509  dvhopvadd  41592  dvhlveclem  41607  dvhopaddN  41613  dicvaddcl  41689  dihopelvalcpre  41747  rtrclex  44068  trclubgNEW  44069  rtrclexi  44072  cnvtrcl0  44077  dfrtrcl5  44080  trcleq2lemRP  44081  trrelind  44116  trrelsuperreldg  44119  trficl  44120  trrelsuperrel2dg  44122  trclrelexplem  44162  relexpaddss  44169  dfrtrcl3  44184  clsneicnv  44556  neicvgnvo  44566  fundcmpsurbijinjpreimafv  47889  fundcmpsurinjALT  47894  rngccoALTV  48769  funcringcsetcALTV2lem9  48796  ringccoALTV  48803  funcringcsetclem9ALTV  48819  fuco112x  49829  fuco22natlem  49842  fucoppcid  49905