Theorem coeq12d 5808

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-br 5094  df-opab 5156  df-co 5628

This theorem is referenced by:  relcnvtrg  6219  xpcoid  6242  csbcog  6249  dfac12lem1  10042  dfac12r  10045  trcleq2lem  14900  trclfvcotrg  14925  relexpaddg  14962  relexpaddd  14963  dfrtrcl2  14971  imasval  17417  cofuval  17791  cofu2nd  17794  cofuval2  17796  cofuass  17798  cofurid  17800  setcco  17992  estrcco  18038  funcestrcsetclem9  18056  funcsetcestrclem9  18071  isdir  18506  smndex1mgm  18817  symgov  19298  funcrngcsetcALT  20558  znval  21474  znle2  21492  evl1fval  22244  mdetfval  22502  mdetdiaglem  22514  ust0  24136  trust  24145  metustexhalf  24472  isngp  24512  ngppropd  24553  tngval  24555  tngngp2  24568  imsval  30667  opsqrlem3  32124  hmopidmch  32135  hmopidmpj  32136  pjidmco  32163  dfpjop  32164  cosnop  32680  tocycfv  33085  cycpm2tr  33095  cyc3genpmlem  33127  cycpmconjslem2  33131  cycpmconjs  33132  cyc3conja  33133  esplyval  33603  zhmnrg  33999  bj-imdirco  37255  dftrrels2  38692  dftrrel2  38694  istendo  40880  tendoco2  40888  tendoidcl  40889  tendococl  40892  tendoplcbv  40895  tendopl2  40897  tendoplco2  40899  tendodi1  40904  tendodi2  40905  tendo0co2  40908  tendoicl  40916  erngplus2  40924  erngplus2-rN  40932  cdlemk55u1  41085  cdlemk55u  41086  dvaplusgv  41130  dvhopvadd  41213  dvhlveclem  41228  dvhopaddN  41234  dicvaddcl  41310  dihopelvalcpre  41368  rtrclex  43735  trclubgNEW  43736  rtrclexi  43739  cnvtrcl0  43744  dfrtrcl5  43747  trcleq2lemRP  43748  trrelind  43783  trrelsuperreldg  43786  trficl  43787  trrelsuperrel2dg  43789  trclrelexplem  43829  relexpaddss  43836  dfrtrcl3  43851  clsneicnv  44223  neicvgnvo  44233  fundcmpsurbijinjpreimafv  47532  fundcmpsurinjALT  47537  rngccoALTV  48396  funcringcsetcALTV2lem9  48423  ringccoALTV  48430  funcringcsetclem9ALTV  48446  fuco112x  49458  fuco22natlem  49471  fucoppcid  49534