Theorem coeq12d 5825

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-br 5111  df-opab 5173  df-co 5647

This theorem is referenced by:  relcnvtrg  6223  xpcoid  6247  csbcog  6254  dfac12lem1  10088  dfac12r  10091  trcleq2lem  14888  trclfvcotrg  14913  relexpaddg  14950  relexpaddd  14951  dfrtrcl2  14959  imasval  17407  cofuval  17782  cofu2nd  17785  cofuval2  17787  cofuass  17789  cofurid  17791  setcco  17983  estrcco  18031  funcestrcsetclem9  18050  funcsetcestrclem9  18065  isdir  18501  smndex1mgm  18731  symgov  19179  znval  20975  znle2  20997  evl1fval  21731  mdetfval  21972  mdetdiaglem  21984  ust0  23608  trust  23618  metustexhalf  23949  isngp  23989  ngppropd  24030  tngval  24032  tngngp2  24053  imsval  29690  opsqrlem3  31147  hmopidmch  31158  hmopidmpj  31159  pjidmco  31186  dfpjop  31187  cosnop  31677  tocycfv  32028  cycpm2tr  32038  cyc3genpmlem  32070  cycpmconjslem2  32074  cycpmconjs  32075  cyc3conja  32076  zhmnrg  32637  bj-imdirco  35734  dftrrels2  37110  dftrrel2  37112  istendo  39296  tendoco2  39304  tendoidcl  39305  tendococl  39308  tendoplcbv  39311  tendopl2  39313  tendoplco2  39315  tendodi1  39320  tendodi2  39321  tendo0co2  39324  tendoicl  39332  erngplus2  39340  erngplus2-rN  39348  cdlemk55u1  39501  cdlemk55u  39502  dvaplusgv  39546  dvhopvadd  39629  dvhlveclem  39644  dvhopaddN  39650  dicvaddcl  39726  dihopelvalcpre  39784  rtrclex  42011  trclubgNEW  42012  rtrclexi  42015  cnvtrcl0  42020  dfrtrcl5  42023  trcleq2lemRP  42024  trrelind  42059  trrelsuperreldg  42062  trficl  42063  trrelsuperrel2dg  42065  trclrelexplem  42105  relexpaddss  42112  dfrtrcl3  42127  clsneicnv  42499  neicvgnvo  42509  fundcmpsurbijinjpreimafv  45719  fundcmpsurinjALT  45724  rngccoALTV  46406  funcrngcsetcALT  46417  funcringcsetcALTV2lem9  46462  ringccoALTV  46469  funcringcsetclem9ALTV  46485