Theorem coeq12d 5286

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

Syntax hints:   → wi 4   = wceq 1483   ∘ ccom 5118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-co 5123

This theorem is referenced by:  xpcoid  5676  dfac12lem1  8965  dfac12r  8968  trcleq2lem  13730  trclfvcotrg  13757  relexpaddg  13793  dfrtrcl2  13802  imasval  16171  cofuval  16542  cofu2nd  16545  cofuval2  16547  cofuass  16549  cofurid  16551  setcco  16733  estrcco  16770  funcestrcsetclem9  16788  funcsetcestrclem9  16803  isdir  17232  evl1fval  19692  znval  19883  znle2  19902  mdetfval  20392  mdetdiaglem  20404  ust0  22023  trust  22033  metustexhalf  22361  isngp  22400  ngppropd  22441  tngval  22443  tngngp2  22456  imsval  27540  opsqrlem3  29001  hmopidmch  29012  hmopidmpj  29013  pjidmco  29040  dfpjop  29041  zhmnrg  30011  istendo  36048  tendoco2  36056  tendoidcl  36057  tendococl  36060  tendoplcbv  36063  tendopl2  36065  tendoplco2  36067  tendodi1  36072  tendodi2  36073  tendo0co2  36076  tendoicl  36084  erngplus2  36092  erngplus2-rN  36100  cdlemk55u1  36253  cdlemk55u  36254  dvaplusgv  36298  dvhopvadd  36382  dvhlveclem  36397  dvhopaddN  36403  dicvaddcl  36479  dihopelvalcpre  36537  rtrclex  37924  trclubgNEW  37925  rtrclexi  37928  cnvtrcl0  37933  dfrtrcl5  37936  trcleq2lemRP  37937  csbcog  37941  trrelind  37957  trrelsuperreldg  37960  trficl  37961  trrelsuperrel2dg  37963  trclrelexplem  38003  relexpaddss  38010  dfrtrcl3  38025  clsneicnv  38403  neicvgnvo  38413  rngccoALTV  41988  funcrngcsetcALT  41999  funcringcsetcALTV2lem9  42044  ringccoALTV  42051  funcringcsetclem9ALTV  42067