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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-br 5099  df-opab 5161  df-co 5633

This theorem is referenced by:  relcnvtrg  6225  xpcoid  6248  csbcog  6255  dfac12lem1  10054  dfac12r  10057  trcleq2lem  14914  trclfvcotrg  14939  relexpaddg  14976  relexpaddd  14977  dfrtrcl2  14985  imasval  17432  cofuval  17806  cofu2nd  17809  cofuval2  17811  cofuass  17813  cofurid  17815  setcco  18007  estrcco  18053  funcestrcsetclem9  18071  funcsetcestrclem9  18086  isdir  18521  smndex1mgm  18832  symgov  19313  funcrngcsetcALT  20574  znval  21490  znle2  21508  evl1fval  22272  mdetfval  22530  mdetdiaglem  22542  ust0  24164  trust  24173  metustexhalf  24500  isngp  24540  ngppropd  24581  tngval  24583  tngngp2  24596  imsval  30760  opsqrlem3  32217  hmopidmch  32228  hmopidmpj  32229  pjidmco  32256  dfpjop  32257  cosnop  32774  tocycfv  33191  cycpm2tr  33201  cyc3genpmlem  33233  cycpmconjslem2  33237  cycpmconjs  33238  cyc3conja  33239  esplyval  33720  zhmnrg  34122  bj-imdirco  37391  dftrrels2  38828  dftrrel2  38830  istendo  41016  tendoco2  41024  tendoidcl  41025  tendococl  41028  tendoplcbv  41031  tendopl2  41033  tendoplco2  41035  tendodi1  41040  tendodi2  41041  tendo0co2  41044  tendoicl  41052  erngplus2  41060  erngplus2-rN  41068  cdlemk55u1  41221  cdlemk55u  41222  dvaplusgv  41266  dvhopvadd  41349  dvhlveclem  41364  dvhopaddN  41370  dicvaddcl  41446  dihopelvalcpre  41504  rtrclex  43854  trclubgNEW  43855  rtrclexi  43858  cnvtrcl0  43863  dfrtrcl5  43866  trcleq2lemRP  43867  trrelind  43902  trrelsuperreldg  43905  trficl  43906  trrelsuperrel2dg  43908  trclrelexplem  43948  relexpaddss  43955  dfrtrcl3  43970  clsneicnv  44342  neicvgnvo  44352  fundcmpsurbijinjpreimafv  47649  fundcmpsurinjALT  47654  rngccoALTV  48513  funcringcsetcALTV2lem9  48540  ringccoALTV  48547  funcringcsetclem9ALTV  48563  fuco112x  49573  fuco22natlem  49586  fucoppcid  49649