Theorem coeq12d 5841

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∘ ccom 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-br 5103  df-opab 5167  df-co 5659

This theorem is used by:  relcnvtrgOLD  6269  xpcoid  6293  csbcog  6300  dfac12lem1  10225  dfac12r  10228  trcleq2lem  15149  trclfvcotrg  15174  relexpaddg  15211  relexpaddd  15212  dfrtrcl2  15220  imasval  17688  cofuval  18062  cofu2nd  18065  cofuval2  18067  cofuass  18069  cofurid  18071  setcco  18263  estrcco  18309  funcestrcsetclem9  18327  funcsetcestrclem9  18342  isdir  18777  smndex1mgm  19111  symgov  19603  funcrngcsetcALT  20898  znval  21846  znle2  21864  evl1fval  22651  mdetfval  22906  mdetdiaglem  22918  ust0  24544  trust  24553  metustexhalf  24880  isngp  24920  ngppropd  24961  tngval  24963  tngngp2  24976  imsval  31292  opsqrlem3  32749  hmopidmch  32760  hmopidmpj  32761  pjidmco  32788  dfpjop  32789  cosnop  33335  tocycfv  33716  cycpm2tr  33726  cyc3genpmlem  33758  cycpmconjslem2  33762  cycpmconjs  33763  cyc3conja  33764  esplyval  34240  zhmnrg  34643  bj-imdirco  38204  dftrrels2  39684  dftrrel2  39686  istendo  41910  tendoco2  41918  tendoidcl  41919  tendococl  41922  tendoplcbv  41925  tendopl2  41927  tendoplco2  41929  tendodi1  41934  tendodi2  41935  tendo0co2  41938  tendoicl  41946  erngplus2  41954  erngplus2-rN  41962  cdlemk55u1  42115  cdlemk55u  42116  dvaplusgv  42160  dvhopvadd  42243  dvhlveclem  42258  dvhopaddN  42264  dicvaddcl  42340  dihopelvalcpre  42398  rtrclex  44710  trclubgNEW  44711  rtrclexi  44714  cnvtrcl0  44719  dfrtrcl5  44722  trcleq2lemRP  44723  trrelind  44758  trrelsuperreldg  44761  trficl  44762  trrelsuperrel2dg  44764  trclrelexplem  44804  relexpaddss  44811  dfrtrcl3  44826  clsneicnv  45198  neicvgnvo  45208  fundcmpsurbijinjpreimafv  48582  fundcmpsurinjALT  48587  rngccoALTV  49461  funcringcsetcALTV2lem9  49488  ringccoALTV  49495  funcringcsetclem9ALTV  49511  fuco112x  50547  fuco22natlem  50560  fucoppcid  50636