Theorem coeq12d 5737

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

Syntax hints:   → wi 4   = wceq 1537   ∘ ccom 5561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954  df-br 5069  df-opab 5131  df-co 5566

This theorem is referenced by:  relcnvtrg  6121  xpcoid  6143  dfac12lem1  9571  dfac12r  9574  trcleq2lem  14353  trclfvcotrg  14378  relexpaddg  14414  dfrtrcl2  14423  imasval  16786  cofuval  17154  cofu2nd  17157  cofuval2  17159  cofuass  17161  cofurid  17163  setcco  17345  estrcco  17382  funcestrcsetclem9  17400  funcsetcestrclem9  17415  isdir  17844  smndex1mgm  18074  symgov  18514  evl1fval  20493  znval  20684  znle2  20702  mdetfval  21197  mdetdiaglem  21209  ust0  22830  trust  22840  metustexhalf  23168  isngp  23207  ngppropd  23248  tngval  23250  tngngp2  23263  imsval  28464  opsqrlem3  29921  hmopidmch  29932  hmopidmpj  29933  pjidmco  29960  dfpjop  29961  cosnop  30433  tocycfv  30753  cycpm2tr  30763  cyc3genpmlem  30795  cycpmconjslem2  30799  cycpmconjs  30800  cyc3conja  30801  zhmnrg  31210  dftrrels2  35813  dftrrel2  35815  istendo  37898  tendoco2  37906  tendoidcl  37907  tendococl  37910  tendoplcbv  37913  tendopl2  37915  tendoplco2  37917  tendodi1  37922  tendodi2  37923  tendo0co2  37926  tendoicl  37934  erngplus2  37942  erngplus2-rN  37950  cdlemk55u1  38103  cdlemk55u  38104  dvaplusgv  38148  dvhopvadd  38231  dvhlveclem  38246  dvhopaddN  38252  dicvaddcl  38328  dihopelvalcpre  38386  rtrclex  39984  trclubgNEW  39985  rtrclexi  39988  cnvtrcl0  39993  dfrtrcl5  39996  trcleq2lemRP  39997  csbcog  40001  trrelind  40017  trrelsuperreldg  40020  trficl  40021  trrelsuperrel2dg  40023  trclrelexplem  40063  relexpaddss  40070  dfrtrcl3  40085  clsneicnv  40462  neicvgnvo  40472  fundcmpsurbijinjpreimafv  43574  fundcmpsurinjALT  43579  rngccoALTV  44266  funcrngcsetcALT  44277  funcringcsetcALTV2lem9  44322  ringccoALTV  44329  funcringcsetclem9ALTV  44345