Theorem coeq12d 5424

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

Syntax hints:   → wi 4   = wceq 1631   ∘ ccom 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-in 3730  df-ss 3737  df-br 4788  df-opab 4848  df-co 5259

This theorem is referenced by:  xpcoid  5819  dfac12lem1  9171  dfac12r  9174  trcleq2lem  13940  trclfvcotrg  13965  relexpaddg  14001  dfrtrcl2  14010  imasval  16379  cofuval  16749  cofu2nd  16752  cofuval2  16754  cofuass  16756  cofurid  16758  setcco  16940  estrcco  16977  funcestrcsetclem9  16996  funcsetcestrclem9  17011  isdir  17440  evl1fval  19907  znval  20098  znle2  20117  mdetfval  20610  mdetdiaglem  20622  ust0  22243  trust  22253  metustexhalf  22581  isngp  22620  ngppropd  22661  tngval  22663  tngngp2  22676  imsval  27880  opsqrlem3  29341  hmopidmch  29352  hmopidmpj  29353  pjidmco  29380  dfpjop  29381  zhmnrg  30351  istendo  36570  tendoco2  36578  tendoidcl  36579  tendococl  36582  tendoplcbv  36585  tendopl2  36587  tendoplco2  36589  tendodi1  36594  tendodi2  36595  tendo0co2  36598  tendoicl  36606  erngplus2  36614  erngplus2-rN  36622  cdlemk55u1  36775  cdlemk55u  36776  dvaplusgv  36820  dvhopvadd  36903  dvhlveclem  36918  dvhopaddN  36924  dicvaddcl  37000  dihopelvalcpre  37058  rtrclex  38450  trclubgNEW  38451  rtrclexi  38454  cnvtrcl0  38459  dfrtrcl5  38462  trcleq2lemRP  38463  csbcog  38467  trrelind  38483  trrelsuperreldg  38486  trficl  38487  trrelsuperrel2dg  38489  trclrelexplem  38529  relexpaddss  38536  dfrtrcl3  38551  clsneicnv  38929  neicvgnvo  38939  rngccoALTV  42513  funcrngcsetcALT  42524  funcringcsetcALTV2lem9  42569  ringccoALTV  42576  funcringcsetclem9ALTV  42592