Theorem coeq12d 5735

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

Syntax hints:   → wi 4   = wceq 1537   ∘ ccom 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5067  df-opab 5129  df-co 5564

This theorem is referenced by:  relcnvtrg  6119  xpcoid  6141  dfac12lem1  9569  dfac12r  9572  trcleq2lem  14351  trclfvcotrg  14376  relexpaddg  14412  dfrtrcl2  14421  imasval  16784  cofuval  17152  cofu2nd  17155  cofuval2  17157  cofuass  17159  cofurid  17161  setcco  17343  estrcco  17380  funcestrcsetclem9  17398  funcsetcestrclem9  17413  isdir  17842  smndex1mgm  18072  symgov  18512  evl1fval  20491  znval  20682  znle2  20700  mdetfval  21195  mdetdiaglem  21207  ust0  22828  trust  22838  metustexhalf  23166  isngp  23205  ngppropd  23246  tngval  23248  tngngp2  23261  imsval  28462  opsqrlem3  29919  hmopidmch  29930  hmopidmpj  29931  pjidmco  29958  dfpjop  29959  cosnop  30431  tocycfv  30751  cycpm2tr  30761  cyc3genpmlem  30793  cycpmconjslem2  30797  cycpmconjs  30798  cyc3conja  30799  zhmnrg  31208  dftrrels2  35826  dftrrel2  35828  istendo  37911  tendoco2  37919  tendoidcl  37920  tendococl  37923  tendoplcbv  37926  tendopl2  37928  tendoplco2  37930  tendodi1  37935  tendodi2  37936  tendo0co2  37939  tendoicl  37947  erngplus2  37955  erngplus2-rN  37963  cdlemk55u1  38116  cdlemk55u  38117  dvaplusgv  38161  dvhopvadd  38244  dvhlveclem  38259  dvhopaddN  38265  dicvaddcl  38341  dihopelvalcpre  38399  rtrclex  39997  trclubgNEW  39998  rtrclexi  40001  cnvtrcl0  40006  dfrtrcl5  40009  trcleq2lemRP  40010  csbcog  40014  trrelind  40030  trrelsuperreldg  40033  trficl  40034  trrelsuperrel2dg  40036  trclrelexplem  40076  relexpaddss  40083  dfrtrcl3  40098  clsneicnv  40475  neicvgnvo  40485  fundcmpsurbijinjpreimafv  43587  fundcmpsurinjALT  43592  rngccoALTV  44279  funcrngcsetcALT  44290  funcringcsetcALTV2lem9  44335  ringccoALTV  44342  funcringcsetclem9ALTV  44358