Theorem ineq12 3677

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 3675	. 2 |- ( A = B -> ( A i^i C ) = ( B i^i C ) )
2		ineq2 3676	. 2 |- ( C = D -> ( B i^i C ) = ( B i^i D ) )
3	1, 2	sylan9eq 2502	1 |- ( ( A = B /\ C = D ) -> ( A i^i C ) = ( B i^i D ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465

This theorem is referenced by:  ineq12i  3680  ineq12d  3683  ineqan12d  3684  fnun  5673  undifixp  7503  endisj  7602  sbthlem8  7632  fiin  7880  pm54.43  8379  kmlem9  8536  indistopon  19368  epttop  19376  restbas  19525  ordtbas2  19558  txbas  19934  ptbasin  19944  trfbas2  20210  snfil  20231  fbasrn  20251  trfil2  20254  fmfnfmlem3  20323  ustuqtop2  20611  minveclem3b  21709  isperp  23954  frrlem4  29358  diophin  30674  kelac2lem  30978