Theorem coeq12d 5811

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

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

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 3922  df-br 5096  df-opab 5158  df-co 5632

This theorem is referenced by:  relcnvtrg  6219  xpcoid  6242  csbcog  6249  dfac12lem1  10057  dfac12r  10060  trcleq2lem  14916  trclfvcotrg  14941  relexpaddg  14978  relexpaddd  14979  dfrtrcl2  14987  imasval  17433  cofuval  17807  cofu2nd  17810  cofuval2  17812  cofuass  17814  cofurid  17816  setcco  18008  estrcco  18054  funcestrcsetclem9  18072  funcsetcestrclem9  18087  isdir  18522  smndex1mgm  18799  symgov  19281  funcrngcsetcALT  20544  znval  21460  znle2  21478  evl1fval  22231  mdetfval  22489  mdetdiaglem  22501  ust0  24123  trust  24133  metustexhalf  24460  isngp  24500  ngppropd  24541  tngval  24543  tngngp2  24556  imsval  30647  opsqrlem3  32104  hmopidmch  32115  hmopidmpj  32116  pjidmco  32143  dfpjop  32144  cosnop  32651  tocycfv  33064  cycpm2tr  33074  cyc3genpmlem  33106  cycpmconjslem2  33110  cycpmconjs  33111  cyc3conja  33112  zhmnrg  33934  bj-imdirco  37166  dftrrels2  38554  dftrrel2  38556  istendo  40742  tendoco2  40750  tendoidcl  40751  tendococl  40754  tendoplcbv  40757  tendopl2  40759  tendoplco2  40761  tendodi1  40766  tendodi2  40767  tendo0co2  40770  tendoicl  40778  erngplus2  40786  erngplus2-rN  40794  cdlemk55u1  40947  cdlemk55u  40948  dvaplusgv  40992  dvhopvadd  41075  dvhlveclem  41090  dvhopaddN  41096  dicvaddcl  41172  dihopelvalcpre  41230  rtrclex  43593  trclubgNEW  43594  rtrclexi  43597  cnvtrcl0  43602  dfrtrcl5  43605  trcleq2lemRP  43606  trrelind  43641  trrelsuperreldg  43644  trficl  43645  trrelsuperrel2dg  43647  trclrelexplem  43687  relexpaddss  43694  dfrtrcl3  43709  clsneicnv  44081  neicvgnvo  44091  fundcmpsurbijinjpreimafv  47395  fundcmpsurinjALT  47400  rngccoALTV  48259  funcringcsetcALTV2lem9  48286  ringccoALTV  48293  funcringcsetclem9ALTV  48309  fuco112x  49321  fuco22natlem  49334  fucoppcid  49397