Theorem coeq12d 5708

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-in 3851  df-ss 3861  df-br 5032  df-opab 5094  df-co 5535

This theorem is referenced by:  relcnvtrg  6100  xpcoid  6123  dfac12lem1  9646  dfac12r  9649  trcleq2lem  14443  trclfvcotrg  14468  relexpaddg  14505  relexpaddd  14506  dfrtrcl2  14514  imasval  16890  cofuval  17260  cofu2nd  17263  cofuval2  17265  cofuass  17267  cofurid  17269  setcco  17458  estrcco  17499  funcestrcsetclem9  17517  funcsetcestrclem9  17532  isdir  17961  smndex1mgm  18191  symgov  18633  znval  20357  znle2  20375  evl1fval  21101  mdetfval  21340  mdetdiaglem  21352  ust0  22974  trust  22984  metustexhalf  23312  isngp  23352  ngppropd  23393  tngval  23395  tngngp2  23408  imsval  28623  opsqrlem3  30080  hmopidmch  30091  hmopidmpj  30092  pjidmco  30119  dfpjop  30120  cosnop  30606  tocycfv  30956  cycpm2tr  30966  cyc3genpmlem  30998  cycpmconjslem2  31002  cycpmconjs  31003  cyc3conja  31004  zhmnrg  31490  bj-imdirco  35005  dftrrels2  36335  dftrrel2  36337  istendo  38420  tendoco2  38428  tendoidcl  38429  tendococl  38432  tendoplcbv  38435  tendopl2  38437  tendoplco2  38439  tendodi1  38444  tendodi2  38445  tendo0co2  38448  tendoicl  38456  erngplus2  38464  erngplus2-rN  38472  cdlemk55u1  38625  cdlemk55u  38626  dvaplusgv  38670  dvhopvadd  38753  dvhlveclem  38768  dvhopaddN  38774  dicvaddcl  38850  dihopelvalcpre  38908  rtrclex  40793  trclubgNEW  40794  rtrclexi  40797  cnvtrcl0  40802  dfrtrcl5  40805  trcleq2lemRP  40806  csbcog  40826  trrelind  40842  trrelsuperreldg  40845  trficl  40846  trrelsuperrel2dg  40848  trclrelexplem  40888  relexpaddss  40895  dfrtrcl3  40910  clsneicnv  41284  neicvgnvo  41294  fundcmpsurbijinjpreimafv  44423  fundcmpsurinjALT  44428  rngccoALTV  45110  funcrngcsetcALT  45121  funcringcsetcALTV2lem9  45166  ringccoALTV  45173  funcringcsetclem9ALTV  45189