Theorem coeq12d 5430

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

Syntax hints:   → wi 4   = wceq 1620   ∘ ccom 5258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-in 3710  df-ss 3717  df-br 4793  df-opab 4853  df-co 5263

This theorem is referenced by:  xpcoid  5825  dfac12lem1  9128  dfac12r  9131  trcleq2lem  13902  trclfvcotrg  13927  relexpaddg  13963  dfrtrcl2  13972  imasval  16344  cofuval  16714  cofu2nd  16717  cofuval2  16719  cofuass  16721  cofurid  16723  setcco  16905  estrcco  16942  funcestrcsetclem9  16960  funcsetcestrclem9  16975  isdir  17404  evl1fval  19865  znval  20056  znle2  20075  mdetfval  20565  mdetdiaglem  20577  ust0  22195  trust  22205  metustexhalf  22533  isngp  22572  ngppropd  22613  tngval  22615  tngngp2  22628  imsval  27820  opsqrlem3  29281  hmopidmch  29292  hmopidmpj  29293  pjidmco  29320  dfpjop  29321  zhmnrg  30291  istendo  36519  tendoco2  36527  tendoidcl  36528  tendococl  36531  tendoplcbv  36534  tendopl2  36536  tendoplco2  36538  tendodi1  36543  tendodi2  36544  tendo0co2  36547  tendoicl  36555  erngplus2  36563  erngplus2-rN  36571  cdlemk55u1  36724  cdlemk55u  36725  dvaplusgv  36769  dvhopvadd  36853  dvhlveclem  36868  dvhopaddN  36874  dicvaddcl  36950  dihopelvalcpre  37008  rtrclex  38395  trclubgNEW  38396  rtrclexi  38399  cnvtrcl0  38404  dfrtrcl5  38407  trcleq2lemRP  38408  csbcog  38412  trrelind  38428  trrelsuperreldg  38431  trficl  38432  trrelsuperrel2dg  38434  trclrelexplem  38474  relexpaddss  38481  dfrtrcl3  38496  clsneicnv  38874  neicvgnvo  38884  rngccoALTV  42467  funcrngcsetcALT  42478  funcringcsetcALTV2lem9  42523  ringccoALTV  42530  funcringcsetclem9ALTV  42546