Theorem coeq12d 5821

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

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5636

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-co 5641

This theorem is referenced by:  relcnvtrg  6233  xpcoid  6256  csbcog  6263  dfac12lem1  10068  dfac12r  10071  trcleq2lem  14955  trclfvcotrg  14980  relexpaddg  15017  relexpaddd  15018  dfrtrcl2  15026  imasval  17477  cofuval  17851  cofu2nd  17854  cofuval2  17856  cofuass  17858  cofurid  17860  setcco  18052  estrcco  18098  funcestrcsetclem9  18116  funcsetcestrclem9  18131  isdir  18566  smndex1mgm  18880  symgov  19361  funcrngcsetcALT  20620  znval  21517  znle2  21535  evl1fval  22295  mdetfval  22553  mdetdiaglem  22565  ust0  24187  trust  24196  metustexhalf  24523  isngp  24563  ngppropd  24604  tngval  24606  tngngp2  24619  imsval  30758  opsqrlem3  32215  hmopidmch  32226  hmopidmpj  32227  pjidmco  32254  dfpjop  32255  cosnop  32770  tocycfv  33172  cycpm2tr  33182  cyc3genpmlem  33214  cycpmconjslem2  33218  cycpmconjs  33219  cyc3conja  33220  esplyval  33708  zhmnrg  34111  bj-imdirco  37506  dftrrels2  38982  dftrrel2  38984  istendo  41208  tendoco2  41216  tendoidcl  41217  tendococl  41220  tendoplcbv  41223  tendopl2  41225  tendoplco2  41227  tendodi1  41232  tendodi2  41233  tendo0co2  41236  tendoicl  41244  erngplus2  41252  erngplus2-rN  41260  cdlemk55u1  41413  cdlemk55u  41414  dvaplusgv  41458  dvhopvadd  41541  dvhlveclem  41556  dvhopaddN  41562  dicvaddcl  41638  dihopelvalcpre  41696  rtrclex  44046  trclubgNEW  44047  rtrclexi  44050  cnvtrcl0  44055  dfrtrcl5  44058  trcleq2lemRP  44059  trrelind  44094  trrelsuperreldg  44097  trficl  44098  trrelsuperrel2dg  44100  trclrelexplem  44140  relexpaddss  44147  dfrtrcl3  44162  clsneicnv  44534  neicvgnvo  44544  fundcmpsurbijinjpreimafv  47869  fundcmpsurinjALT  47874  rngccoALTV  48749  funcringcsetcALTV2lem9  48776  ringccoALTV  48783  funcringcsetclem9ALTV  48799  fuco112x  49809  fuco22natlem  49822  fucoppcid  49885