Theorem coeq12d 5842

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-co 5660

This theorem is used by:  relcnvtrgOLD  6262  xpcoid  6286  csbcog  6293  dfac12lem1  10203  dfac12r  10206  trcleq2lem  15124  trclfvcotrg  15149  relexpaddg  15186  relexpaddd  15187  dfrtrcl2  15195  imasval  17663  cofuval  18037  cofu2nd  18040  cofuval2  18042  cofuass  18044  cofurid  18046  setcco  18238  estrcco  18284  funcestrcsetclem9  18302  funcsetcestrclem9  18317  isdir  18752  smndex1mgm  19086  symgov  19578  funcrngcsetcALT  20873  znval  21821  znle2  21839  evl1fval  22626  mdetfval  22881  mdetdiaglem  22893  ust0  24519  trust  24528  metustexhalf  24855  isngp  24895  ngppropd  24936  tngval  24938  tngngp2  24951  imsval  31269  opsqrlem3  32726  hmopidmch  32737  hmopidmpj  32738  pjidmco  32765  dfpjop  32766  cosnop  33270  tocycfv  33652  cycpm2tr  33662  cyc3genpmlem  33694  cycpmconjslem2  33698  cycpmconjs  33699  cyc3conja  33700  esplyval  34176  zhmnrg  34579  bj-imdirco  38079  dftrrels2  39559  dftrrel2  39561  istendo  41785  tendoco2  41793  tendoidcl  41794  tendococl  41797  tendoplcbv  41800  tendopl2  41802  tendoplco2  41804  tendodi1  41809  tendodi2  41810  tendo0co2  41813  tendoicl  41821  erngplus2  41829  erngplus2-rN  41837  cdlemk55u1  41990  cdlemk55u  41991  dvaplusgv  42035  dvhopvadd  42118  dvhlveclem  42133  dvhopaddN  42139  dicvaddcl  42215  dihopelvalcpre  42273  rtrclex  44576  trclubgNEW  44577  rtrclexi  44580  cnvtrcl0  44585  dfrtrcl5  44588  trcleq2lemRP  44589  trrelind  44624  trrelsuperreldg  44627  trficl  44628  trrelsuperrel2dg  44630  trclrelexplem  44670  relexpaddss  44677  dfrtrcl3  44692  clsneicnv  45064  neicvgnvo  45074  fundcmpsurbijinjpreimafv  48433  fundcmpsurinjALT  48438  rngccoALTV  49312  funcringcsetcALTV2lem9  49339  ringccoALTV  49346  funcringcsetclem9ALTV  49362  fuco112x  50384  fuco22natlem  50397  fucoppcid  50460