Theorem coeq12d 5841

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

Syntax hints:   → wi 4   = wceq 1563   ∘ ccom 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-br 5106  df-opab 5168  df-co 5661

This theorem is referenced by:  relcnvtrg  6258  xpcoid  6281  csbcog  6288  dfac12lem1  10115  dfac12r  10118  trcleq2lem  15018  trclfvcotrg  15043  relexpaddg  15080  relexpaddd  15081  dfrtrcl2  15089  imasval  17555  cofuval  17929  cofu2nd  17932  cofuval2  17934  cofuass  17936  cofurid  17938  setcco  18130  estrcco  18176  funcestrcsetclem9  18194  funcsetcestrclem9  18209  isdir  18644  smndex1mgm  18959  symgov  19445  funcrngcsetcALT  20717  znval  21645  znle2  21663  evl1fval  22449  mdetfval  22704  mdetdiaglem  22716  ust0  24338  trust  24347  metustexhalf  24674  isngp  24714  ngppropd  24755  tngval  24757  tngngp2  24770  imsval  30946  opsqrlem3  32403  hmopidmch  32414  hmopidmpj  32415  pjidmco  32442  dfpjop  32443  cosnop  32952  tocycfv  33342  cycpm2tr  33352  cyc3genpmlem  33384  cycpmconjslem2  33388  cycpmconjs  33389  cyc3conja  33390  esplyval  33869  zhmnrg  34272  bj-imdirco  37694  dftrrels2  39170  dftrrel2  39172  istendo  41396  tendoco2  41404  tendoidcl  41405  tendococl  41408  tendoplcbv  41411  tendopl2  41413  tendoplco2  41415  tendodi1  41420  tendodi2  41421  tendo0co2  41424  tendoicl  41432  erngplus2  41440  erngplus2-rN  41448  cdlemk55u1  41601  cdlemk55u  41602  dvaplusgv  41646  dvhopvadd  41729  dvhlveclem  41744  dvhopaddN  41750  dicvaddcl  41826  dihopelvalcpre  41884  rtrclex  44205  trclubgNEW  44206  rtrclexi  44209  cnvtrcl0  44214  dfrtrcl5  44217  trcleq2lemRP  44218  trrelind  44253  trrelsuperreldg  44256  trficl  44257  trrelsuperrel2dg  44259  trclrelexplem  44299  relexpaddss  44306  dfrtrcl3  44321  clsneicnv  44693  neicvgnvo  44703  fundcmpsurbijinjpreimafv  48011  fundcmpsurinjALT  48016  rngccoALTV  48891  funcringcsetcALTV2lem9  48918  ringccoALTV  48925  funcringcsetclem9ALTV  48941  fuco112x  49961  fuco22natlem  49974  fucoppcid  50037