Theorem coeq12d 5877

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

Syntax hints:   → wi 4   = wceq 1536   ∘ ccom 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-co 5697

This theorem is referenced by:  relcnvtrg  6287  xpcoid  6311  csbcog  6318  dfac12lem1  10181  dfac12r  10184  trcleq2lem  15026  trclfvcotrg  15051  relexpaddg  15088  relexpaddd  15089  dfrtrcl2  15097  imasval  17557  cofuval  17932  cofu2nd  17935  cofuval2  17937  cofuass  17939  cofurid  17941  setcco  18136  estrcco  18184  funcestrcsetclem9  18203  funcsetcestrclem9  18218  isdir  18655  smndex1mgm  18932  symgov  19415  funcrngcsetcALT  20657  znval  21567  znle2  21589  evl1fval  22347  mdetfval  22607  mdetdiaglem  22619  ust0  24243  trust  24253  metustexhalf  24584  isngp  24624  ngppropd  24665  tngval  24667  tngngp2  24688  imsval  30713  opsqrlem3  32170  hmopidmch  32181  hmopidmpj  32182  pjidmco  32209  dfpjop  32210  cosnop  32709  tocycfv  33111  cycpm2tr  33121  cyc3genpmlem  33153  cycpmconjslem2  33157  cycpmconjs  33158  cyc3conja  33159  zhmnrg  33927  bj-imdirco  37172  dftrrels2  38556  dftrrel2  38558  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  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  47331  fundcmpsurinjALT  47336  rngccoALTV  48114  funcringcsetcALTV2lem9  48141  ringccoALTV  48148  funcringcsetclem9ALTV  48164