Theorem ineq2d 3361

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)

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 3355	. 2 |- ( A = B -> ( C i^i A ) = ( C i^i B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C i^i A ) = ( C i^i B ) )

Syntax hints:   -> wi 4   = wceq 1364   i^i cin 3153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3160

This theorem is referenced by:  disjpr2  3683  rint0  3910  riin0  3985  disji2  4023  xpriindim  4801  riinint  4924  reseq2  4938  csbresg  4946  resindm  4985  isoselem  5864  zfz1isolem1  10914  fsumm1  11562  ennnfonelemhf1o  12573  nninfdclemcl  12608  nninfdclemp1  12610  nninfdc  12613  ressvalsets  12685  ressbasd  12688  ressinbasd  12695  ressressg  12696  restval  12859  mgpress  13430  subrngpropd  13715  subrgpropd  13752  crng2idl  14030  basis1  14226  baspartn  14229  eltg  14231  tgdom  14251  ntrval  14289  resttopon2  14357  restopnb  14360  qtopbasss  14700