Theorem coeq12d 5699

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

Syntax hints:   → wi 4   = wceq 1538   ∘ ccom 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-co 5528

This theorem is referenced by:  relcnvtrg  6086  xpcoid  6109  dfac12lem1  9554  dfac12r  9557  trcleq2lem  14342  trclfvcotrg  14367  relexpaddg  14404  relexpaddd  14405  dfrtrcl2  14413  imasval  16776  cofuval  17144  cofu2nd  17147  cofuval2  17149  cofuass  17151  cofurid  17153  setcco  17335  estrcco  17372  funcestrcsetclem9  17390  funcsetcestrclem9  17405  isdir  17834  smndex1mgm  18064  symgov  18504  znval  20227  znle2  20245  evl1fval  20952  mdetfval  21191  mdetdiaglem  21203  ust0  22825  trust  22835  metustexhalf  23163  isngp  23202  ngppropd  23243  tngval  23245  tngngp2  23258  imsval  28468  opsqrlem3  29925  hmopidmch  29936  hmopidmpj  29937  pjidmco  29964  dfpjop  29965  cosnop  30455  tocycfv  30801  cycpm2tr  30811  cyc3genpmlem  30843  cycpmconjslem2  30847  cycpmconjs  30848  cyc3conja  30849  zhmnrg  31318  bj-imdirco  34605  dftrrels2  35971  dftrrel2  35973  istendo  38056  tendoco2  38064  tendoidcl  38065  tendococl  38068  tendoplcbv  38071  tendopl2  38073  tendoplco2  38075  tendodi1  38080  tendodi2  38081  tendo0co2  38084  tendoicl  38092  erngplus2  38100  erngplus2-rN  38108  cdlemk55u1  38261  cdlemk55u  38262  dvaplusgv  38306  dvhopvadd  38389  dvhlveclem  38404  dvhopaddN  38410  dicvaddcl  38486  dihopelvalcpre  38544  rtrclex  40317  trclubgNEW  40318  rtrclexi  40321  cnvtrcl0  40326  dfrtrcl5  40329  trcleq2lemRP  40330  csbcog  40350  trrelind  40366  trrelsuperreldg  40369  trficl  40370  trrelsuperrel2dg  40372  trclrelexplem  40412  relexpaddss  40419  dfrtrcl3  40434  clsneicnv  40808  neicvgnvo  40818  fundcmpsurbijinjpreimafv  43924  fundcmpsurinjALT  43929  rngccoALTV  44612  funcrngcsetcALT  44623  funcringcsetcALTV2lem9  44668  ringccoALTV  44675  funcringcsetclem9ALTV  44691