Theorem coeq12d 5828

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

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  relcnvtrg  6239  xpcoid  6263  csbcog  6270  dfac12lem1  10097  dfac12r  10100  trcleq2lem  14957  trclfvcotrg  14982  relexpaddg  15019  relexpaddd  15020  dfrtrcl2  15028  imasval  17474  cofuval  17844  cofu2nd  17847  cofuval2  17849  cofuass  17851  cofurid  17853  setcco  18045  estrcco  18091  funcestrcsetclem9  18109  funcsetcestrclem9  18124  isdir  18557  smndex1mgm  18834  symgov  19314  funcrngcsetcALT  20550  znval  21445  znle2  21463  evl1fval  22215  mdetfval  22473  mdetdiaglem  22485  ust0  24107  trust  24117  metustexhalf  24444  isngp  24484  ngppropd  24525  tngval  24527  tngngp2  24540  imsval  30614  opsqrlem3  32071  hmopidmch  32082  hmopidmpj  32083  pjidmco  32110  dfpjop  32111  cosnop  32618  tocycfv  33066  cycpm2tr  33076  cyc3genpmlem  33108  cycpmconjslem2  33112  cycpmconjs  33113  cyc3conja  33114  zhmnrg  33955  bj-imdirco  37178  dftrrels2  38566  dftrrel2  38568  istendo  40754  tendoco2  40762  tendoidcl  40763  tendococl  40766  tendoplcbv  40769  tendopl2  40771  tendoplco2  40773  tendodi1  40778  tendodi2  40779  tendo0co2  40782  tendoicl  40790  erngplus2  40798  erngplus2-rN  40806  cdlemk55u1  40959  cdlemk55u  40960  dvaplusgv  41004  dvhopvadd  41087  dvhlveclem  41102  dvhopaddN  41108  dicvaddcl  41184  dihopelvalcpre  41242  rtrclex  43606  trclubgNEW  43607  rtrclexi  43610  cnvtrcl0  43615  dfrtrcl5  43618  trcleq2lemRP  43619  trrelind  43654  trrelsuperreldg  43657  trficl  43658  trrelsuperrel2dg  43660  trclrelexplem  43700  relexpaddss  43707  dfrtrcl3  43722  clsneicnv  44094  neicvgnvo  44104  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjALT  47413  rngccoALTV  48259  funcringcsetcALTV2lem9  48286  ringccoALTV  48293  funcringcsetclem9ALTV  48309  fuco112x  49321  fuco22natlem  49334  fucoppcid  49397