Theorem coeq12d 5849

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∘ ccom 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5107  df-opab 5172  df-co 5665

This theorem is used by:  relcnvtrgOLD  6288  xpcoid  6314  csbcog  6321  dfac12lem1  10252  dfac12r  10255  trcleq2lem  15176  trclfvcotrg  15201  relexpaddg  15238  relexpaddd  15239  dfrtrcl2  15247  imasval  17715  cofuval  18089  cofu2nd  18092  cofuval2  18094  cofuass  18096  cofurid  18098  setcco  18290  estrcco  18336  funcestrcsetclem9  18354  funcsetcestrclem9  18369  isdir  18804  smndex1mgm  19138  symgov  19631  funcrngcsetcALT  20926  znval  21874  znle2  21892  evl1fval  22679  mdetfval  22934  mdetdiaglem  22946  ust0  24572  trust  24581  metustexhalf  24908  isngp  24948  ngppropd  24989  tngval  24991  tngngp2  25004  imsval  31320  opsqrlem3  32777  hmopidmch  32788  hmopidmpj  32789  pjidmco  32816  dfpjop  32817  cosnop  33362  tocycfv  33746  cycpm2tr  33756  cyc3genpmlem  33788  cycpmconjslem2  33792  cycpmconjs  33793  cyc3conja  33794  esplyval  34277  zhmnrg  34680  bj-imdirco  38316  dftrrels2  39794  dftrrel2  39796  istendo  42020  tendoco2  42028  tendoidcl  42029  tendococl  42032  tendoplcbv  42035  tendopl2  42037  tendoplco2  42039  tendodi1  42044  tendodi2  42045  tendo0co2  42048  tendoicl  42056  erngplus2  42064  erngplus2-rN  42072  cdlemk55u1  42225  cdlemk55u  42226  dvaplusgv  42270  dvhopvadd  42353  dvhlveclem  42368  dvhopaddN  42374  dicvaddcl  42450  dihopelvalcpre  42508  rtrclex  44820  trclubgNEW  44821  rtrclexi  44824  cnvtrcl0  44829  dfrtrcl5  44832  trcleq2lemRP  44833  trrelind  44868  trrelsuperreldg  44871  trficl  44872  trrelsuperrel2dg  44874  trclrelexplem  44914  relexpaddss  44921  dfrtrcl3  44936  clsneicnv  45308  neicvgnvo  45318  fundcmpsurbijinjpreimafv  48704  fundcmpsurinjALT  48709  rngccoALTV  49583  funcringcsetcALTV2lem9  49610  ringccoALTV  49617  funcringcsetclem9ALTV  49633  fuco112x  50669  fuco22natlem  50682  fucoppcid  50758