Theorem ineq12 3542

Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)

Assertion

Ref	Expression
ineq12	|- ( ( A = B /\ C = D ) -> ( A i^i C ) = ( B i^i D ) )

Proof of Theorem ineq12

Step	Hyp	Ref	Expression
1		ineq1 3540	. 2 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )
2		ineq2 3541	. 2 |- ( C = D -> ( B i^i C ) = ( B i^i D ) )
3	1, 2	sylan9eq 2490	1 |- ( ( A = B /\ C = D ) -> ( A i^i C ) = ( B i^i D ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   i^i cin 3322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330

This theorem is referenced by:  ineq12i  3545  ineq12d  3548  ineqan12d  3549  fnun  5512  undifixp  7291  endisj  7390  sbthlem8  7420  fiin  7664  pm54.43  8162  kmlem9  8319  indistopon  18580  epttop  18588  restbas  18737  ordtbas2  18770  txbas  19115  ptbasin  19125  trfbas2  19391  snfil  19412  fbasrn  19432  trfil2  19435  fmfnfmlem3  19504  ustuqtop2  19792  minveclem3b  20890  frrlem4  27722  diophin  29064  kelac2lem  29370