Theorem coeq12d 5208

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

Syntax hints:   → wi 4   = wceq 1475   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-co 5047

This theorem is referenced by:  xpcoid  5593  dfac12lem1  8848  dfac12r  8851  trcleq2lem  13578  trclfvcotrg  13605  relexpaddg  13641  dfrtrcl2  13650  imasval  15994  cofuval  16365  cofu2nd  16368  cofuval2  16370  cofuass  16372  cofurid  16374  setcco  16556  estrcco  16593  funcestrcsetclem9  16611  funcsetcestrclem9  16626  isdir  17055  evl1fval  19513  znval  19702  znle2  19721  mdetfval  20211  mdetdiaglem  20223  ust0  21833  trust  21843  metustexhalf  22171  isngp  22210  ngppropd  22251  tngval  22253  tngngp2  22266  imsval  26924  opsqrlem3  28385  hmopidmch  28396  hmopidmpj  28397  pjidmco  28424  dfpjop  28425  zhmnrg  29339  istendo  35066  tendoco2  35074  tendoidcl  35075  tendococl  35078  tendoplcbv  35081  tendopl2  35083  tendoplco2  35085  tendodi1  35090  tendodi2  35091  tendo0co2  35094  tendoicl  35102  erngplus2  35110  erngplus2-rN  35118  cdlemk55u1  35271  cdlemk55u  35272  dvaplusgv  35316  dvhopvadd  35400  dvhlveclem  35415  dvhopaddN  35421  dicvaddcl  35497  dihopelvalcpre  35555  rtrclex  36943  trclubgNEW  36944  rtrclexi  36947  cnvtrcl0  36952  dfrtrcl5  36955  trcleq2lemRP  36956  csbcog  36960  trrelind  36976  trrelsuperreldg  36979  trficl  36980  trrelsuperrel2dg  36982  trclrelexplem  37022  relexpaddss  37029  dfrtrcl3  37044  clsneicnv  37423  neicvgnvo  37433  rngccoALTV  41780  funcrngcsetcALT  41791  funcringcsetcALTV2lem9  41836  ringccoALTV  41843  funcringcsetclem9ALTV  41859