Theorem ineq2d 2796

Description: Equality deduction for intersection of two classes.

Hypothesis

Ref	Expression
ineq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
ineq2d	|- (ph -> (C i^i A) = (C i^i B))

Proof of Theorem ineq2d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 |- (ph -> A = B)
2		ineq2 2790	. 2 |- (A = B -> (C i^i A) = (C i^i B))
3	1, 2	syl 12	1 |- (ph -> (C i^i A) = (C i^i B))

Syntax hints:   -> wi 3   = wceq 1298   i^i cin 2592

This theorem is referenced by:  ineq12dOLD 2798  frirr 3634  fr2nr 3635  fr3nr 3859  reseq2 4219  resdisjOLD 4341  isofrlem 4878  oev2 5207  kmlem11 5937  basis1 8883  eltg 8888  indistop 8918  clslp 9024  metssba 9086  bcthlem15 9291  basmetres 10185  elfg 10284  omlsi 10879  pjoml 10902  chdmj3 11087  chdmj4 11088  ledi 11096  cmbr 11160  cmbr3 11184  pjoml3 11188  fh1 11194  fh2 11195  dmdbr 11871  dmdmd 11872  dmdbr5 11880  dmdsl3 11887  irredlem2 11963  irredlem3 11964  dmdbr6ati 11995  bnj1326 13496  predeq1 13881  predeq3 13883  predep 13903  moec 14351  domrancur1c 14550  valtar 15260  topbnd 15408  opnbnd 15409  cldbnd 15410  subsubtop 15423  cnsubsp2 15427  compsub 15431  reconnlem1 15446  neifg 15559  fcluscomplem 15620  isfclusf 15625  fclsfneii 15628  subspabs 15840  heiborlem25 15979  heiborlem26 15980  pmapglb2 17253  pmapglb2x 17254  pmod 17311  polval 17318  polat 17341  trnset 17405

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603

Copyright terms: Public domain