Theorem coeq12d 5848

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∘ ccom 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-br 5108  df-opab 5172  df-co 5668

This theorem is used by:  relcnvtrgOLD  6268  xpcoid  6292  csbcog  6299  dfac12lem1  10150  dfac12r  10153  trcleq2lem  15068  trclfvcotrg  15093  relexpaddg  15130  relexpaddd  15131  dfrtrcl2  15139  imasval  17603  cofuval  17977  cofu2nd  17980  cofuval2  17982  cofuass  17984  cofurid  17986  setcco  18178  estrcco  18224  funcestrcsetclem9  18242  funcsetcestrclem9  18257  isdir  18692  smndex1mgm  19025  symgov  19517  funcrngcsetcALT  20809  znval  21754  znle2  21772  evl1fval  22559  mdetfval  22814  mdetdiaglem  22826  ust0  24452  trust  24461  metustexhalf  24788  isngp  24828  ngppropd  24869  tngval  24871  tngngp2  24884  imsval  31174  opsqrlem3  32631  hmopidmch  32642  hmopidmpj  32643  pjidmco  32670  dfpjop  32671  cosnop  33175  tocycfv  33557  cycpm2tr  33567  cyc3genpmlem  33599  cycpmconjslem2  33603  cycpmconjs  33604  cyc3conja  33605  esplyval  34080  zhmnrg  34483  bj-imdirco  37950  dftrrels2  39415  dftrrel2  39417  istendo  41641  tendoco2  41649  tendoidcl  41650  tendococl  41653  tendoplcbv  41656  tendopl2  41658  tendoplco2  41660  tendodi1  41665  tendodi2  41666  tendo0co2  41669  tendoicl  41677  erngplus2  41685  erngplus2-rN  41693  cdlemk55u1  41846  cdlemk55u  41847  dvaplusgv  41891  dvhopvadd  41974  dvhlveclem  41989  dvhopaddN  41995  dicvaddcl  42071  dihopelvalcpre  42129  rtrclex  44465  trclubgNEW  44466  rtrclexi  44469  cnvtrcl0  44474  dfrtrcl5  44477  trcleq2lemRP  44478  trrelind  44513  trrelsuperreldg  44516  trficl  44517  trrelsuperrel2dg  44519  trclrelexplem  44559  relexpaddss  44566  dfrtrcl3  44581  clsneicnv  44953  neicvgnvo  44963  fundcmpsurbijinjpreimafv  48315  fundcmpsurinjALT  48320  rngccoALTV  49194  funcringcsetcALTV2lem9  49221  ringccoALTV  49228  funcringcsetclem9ALTV  49244  fuco112x  50266  fuco22natlem  50279  fucoppcid  50342