Theorem coeq12d 5819

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

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5635

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-co 5640

This theorem is referenced by:  relcnvtrg  6231  xpcoid  6254  csbcog  6261  dfac12lem1  10066  dfac12r  10069  trcleq2lem  14953  trclfvcotrg  14978  relexpaddg  15015  relexpaddd  15016  dfrtrcl2  15024  imasval  17475  cofuval  17849  cofu2nd  17852  cofuval2  17854  cofuass  17856  cofurid  17858  setcco  18050  estrcco  18096  funcestrcsetclem9  18114  funcsetcestrclem9  18129  isdir  18564  smndex1mgm  18878  symgov  19359  funcrngcsetcALT  20618  znval  21515  znle2  21533  evl1fval  22293  mdetfval  22551  mdetdiaglem  22563  ust0  24185  trust  24194  metustexhalf  24521  isngp  24561  ngppropd  24602  tngval  24604  tngngp2  24617  imsval  30756  opsqrlem3  32213  hmopidmch  32224  hmopidmpj  32225  pjidmco  32252  dfpjop  32253  cosnop  32768  tocycfv  33170  cycpm2tr  33180  cyc3genpmlem  33212  cycpmconjslem2  33216  cycpmconjs  33217  cyc3conja  33218  esplyval  33706  zhmnrg  34109  bj-imdirco  37504  dftrrels2  38980  dftrrel2  38982  istendo  41206  tendoco2  41214  tendoidcl  41215  tendococl  41218  tendoplcbv  41221  tendopl2  41223  tendoplco2  41225  tendodi1  41230  tendodi2  41231  tendo0co2  41234  tendoicl  41242  erngplus2  41250  erngplus2-rN  41258  cdlemk55u1  41411  cdlemk55u  41412  dvaplusgv  41456  dvhopvadd  41539  dvhlveclem  41554  dvhopaddN  41560  dicvaddcl  41636  dihopelvalcpre  41694  rtrclex  44044  trclubgNEW  44045  rtrclexi  44048  cnvtrcl0  44053  dfrtrcl5  44056  trcleq2lemRP  44057  trrelind  44092  trrelsuperreldg  44095  trficl  44096  trrelsuperrel2dg  44098  trclrelexplem  44138  relexpaddss  44145  dfrtrcl3  44160  clsneicnv  44532  neicvgnvo  44542  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjALT  47872  rngccoALTV  48747  funcringcsetcALTV2lem9  48774  ringccoALTV  48781  funcringcsetclem9ALTV  48797  fuco112x  49807  fuco22natlem  49820  fucoppcid  49883