Theorem ineq12 3691

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478

This theorem is referenced by:  ineq12i  3694  ineq12d  3697  ineqan12d  3698  fnun  5693  undifixp  7524  endisj  7623  sbthlem8  7653  fiin  7900  pm54.43  8398  kmlem9  8555  indistopon  19629  epttop  19637  restbas  19786  ordtbas2  19819  txbas  20194  ptbasin  20204  trfbas2  20470  snfil  20491  fbasrn  20511  trfil2  20514  fmfnfmlem3  20583  ustuqtop2  20871  minveclem3b  21969  isperp  24215  frrlem4  29607  diophin  30911  kelac2lem  31214