Theorem coeq12d 5867

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

Syntax hints:   → wi 4   = wceq 1533   ∘ ccom 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ss 3961  df-br 5150  df-opab 5212  df-co 5687

This theorem is referenced by:  relcnvtrg  6272  xpcoid  6296  csbcog  6303  dfac12lem1  10168  dfac12r  10171  trcleq2lem  14974  trclfvcotrg  14999  relexpaddg  15036  relexpaddd  15037  dfrtrcl2  15045  imasval  17496  cofuval  17871  cofu2nd  17874  cofuval2  17876  cofuass  17878  cofurid  17880  setcco  18075  estrcco  18123  funcestrcsetclem9  18142  funcsetcestrclem9  18157  isdir  18593  smndex1mgm  18867  symgov  19350  funcrngcsetcALT  20586  znval  21482  znle2  21504  evl1fval  22272  mdetfval  22532  mdetdiaglem  22544  ust0  24168  trust  24178  metustexhalf  24509  isngp  24549  ngppropd  24590  tngval  24592  tngngp2  24613  imsval  30567  opsqrlem3  32024  hmopidmch  32035  hmopidmpj  32036  pjidmco  32063  dfpjop  32064  cosnop  32557  tocycfv  32922  cycpm2tr  32932  cyc3genpmlem  32964  cycpmconjslem2  32968  cycpmconjs  32969  cyc3conja  32970  zhmnrg  33696  bj-imdirco  36797  dftrrels2  38174  dftrrel2  38176  istendo  40360  tendoco2  40368  tendoidcl  40369  tendococl  40372  tendoplcbv  40375  tendopl2  40377  tendoplco2  40379  tendodi1  40384  tendodi2  40385  tendo0co2  40388  tendoicl  40396  erngplus2  40404  erngplus2-rN  40412  cdlemk55u1  40565  cdlemk55u  40566  dvaplusgv  40610  dvhopvadd  40693  dvhlveclem  40708  dvhopaddN  40714  dicvaddcl  40790  dihopelvalcpre  40848  rtrclex  43186  trclubgNEW  43187  rtrclexi  43190  cnvtrcl0  43195  dfrtrcl5  43198  trcleq2lemRP  43199  trrelind  43234  trrelsuperreldg  43237  trficl  43238  trrelsuperrel2dg  43240  trclrelexplem  43280  relexpaddss  43287  dfrtrcl3  43302  clsneicnv  43674  neicvgnvo  43684  fundcmpsurbijinjpreimafv  46881  fundcmpsurinjALT  46886  rngccoALTV  47516  funcringcsetcALTV2lem9  47543  ringccoALTV  47550  funcringcsetclem9ALTV  47566