Theorem coeq12d 5776

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

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-br 5076  df-opab 5138  df-co 5599

This theorem is referenced by:  relcnvtrg  6174  xpcoid  6197  csbcog  6204  dfac12lem1  9908  dfac12r  9911  trcleq2lem  14711  trclfvcotrg  14736  relexpaddg  14773  relexpaddd  14774  dfrtrcl2  14782  imasval  17231  cofuval  17606  cofu2nd  17609  cofuval2  17611  cofuass  17613  cofurid  17615  setcco  17807  estrcco  17855  funcestrcsetclem9  17874  funcsetcestrclem9  17889  isdir  18325  smndex1mgm  18555  symgov  19000  znval  20748  znle2  20770  evl1fval  21503  mdetfval  21744  mdetdiaglem  21756  ust0  23380  trust  23390  metustexhalf  23721  isngp  23761  ngppropd  23802  tngval  23804  tngngp2  23825  imsval  29056  opsqrlem3  30513  hmopidmch  30524  hmopidmpj  30525  pjidmco  30552  dfpjop  30553  cosnop  31037  tocycfv  31385  cycpm2tr  31395  cyc3genpmlem  31427  cycpmconjslem2  31431  cycpmconjs  31432  cyc3conja  31433  zhmnrg  31926  bj-imdirco  35370  dftrrels2  36696  dftrrel2  36698  istendo  38781  tendoco2  38789  tendoidcl  38790  tendococl  38793  tendoplcbv  38796  tendopl2  38798  tendoplco2  38800  tendodi1  38805  tendodi2  38806  tendo0co2  38809  tendoicl  38817  erngplus2  38825  erngplus2-rN  38833  cdlemk55u1  38986  cdlemk55u  38987  dvaplusgv  39031  dvhopvadd  39114  dvhlveclem  39129  dvhopaddN  39135  dicvaddcl  39211  dihopelvalcpre  39269  rtrclex  41232  trclubgNEW  41233  rtrclexi  41236  cnvtrcl0  41241  dfrtrcl5  41244  trcleq2lemRP  41245  trrelind  41280  trrelsuperreldg  41283  trficl  41284  trrelsuperrel2dg  41286  trclrelexplem  41326  relexpaddss  41333  dfrtrcl3  41348  clsneicnv  41722  neicvgnvo  41732  fundcmpsurbijinjpreimafv  44870  fundcmpsurinjALT  44875  rngccoALTV  45557  funcrngcsetcALT  45568  funcringcsetcALTV2lem9  45613  ringccoALTV  45620  funcringcsetclem9ALTV  45636