Theorem ineq12 3648

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-in 3436

This theorem is referenced by:  ineq12i  3651  ineq12d  3654  ineqan12d  3655  fnun  5618  undifixp  7402  endisj  7501  sbthlem8  7531  fiin  7776  pm54.43  8274  kmlem9  8431  indistopon  18730  epttop  18738  restbas  18887  ordtbas2  18920  txbas  19265  ptbasin  19275  trfbas2  19541  snfil  19562  fbasrn  19582  trfil2  19585  fmfnfmlem3  19654  ustuqtop2  19942  minveclem3b  21040  isperp  23241  frrlem4  27908  diophin  29252  kelac2lem  29558