Theorem coeq12d 5855

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-br 5115  df-opab 5179  df-co 5675

This theorem is used by:  relcnvtrgOLD  6274  xpcoid  6298  csbcog  6305  dfac12lem1  10146  dfac12r  10149  trcleq2lem  15054  trclfvcotrg  15079  relexpaddg  15116  relexpaddd  15117  dfrtrcl2  15125  imasval  17590  cofuval  17964  cofu2nd  17967  cofuval2  17969  cofuass  17971  cofurid  17973  setcco  18165  estrcco  18211  funcestrcsetclem9  18229  funcsetcestrclem9  18244  isdir  18679  smndex1mgm  19000  symgov  19485  funcrngcsetcALT  20777  znval  21722  znle2  21740  evl1fval  22525  mdetfval  22780  mdetdiaglem  22792  ust0  24414  trust  24423  metustexhalf  24750  isngp  24790  ngppropd  24831  tngval  24833  tngngp2  24846  imsval  31074  opsqrlem3  32531  hmopidmch  32542  hmopidmpj  32543  pjidmco  32570  dfpjop  32571  cosnop  33077  tocycfv  33460  cycpm2tr  33470  cyc3genpmlem  33502  cycpmconjslem2  33506  cycpmconjs  33507  cyc3conja  33508  esplyval  33983  zhmnrg  34386  bj-imdirco  37875  dftrrels2  39349  dftrrel2  39351  istendo  41575  tendoco2  41583  tendoidcl  41584  tendococl  41587  tendoplcbv  41590  tendopl2  41592  tendoplco2  41594  tendodi1  41599  tendodi2  41600  tendo0co2  41603  tendoicl  41611  erngplus2  41619  erngplus2-rN  41627  cdlemk55u1  41780  cdlemk55u  41781  dvaplusgv  41825  dvhopvadd  41908  dvhlveclem  41923  dvhopaddN  41929  dicvaddcl  42005  dihopelvalcpre  42063  rtrclex  44384  trclubgNEW  44385  rtrclexi  44388  cnvtrcl0  44393  dfrtrcl5  44396  trcleq2lemRP  44397  trrelind  44432  trrelsuperreldg  44435  trficl  44436  trrelsuperrel2dg  44438  trclrelexplem  44478  relexpaddss  44485  dfrtrcl3  44500  clsneicnv  44872  neicvgnvo  44882  fundcmpsurbijinjpreimafv  48197  fundcmpsurinjALT  48202  rngccoALTV  49077  funcringcsetcALTV2lem9  49104  ringccoALTV  49111  funcringcsetclem9ALTV  49127  fuco112x  50151  fuco22natlem  50164  fucoppcid  50227