Theorem ineq12 3631

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

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1446   i^i cin 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-in 3413

This theorem is referenced by:  ineq12i  3634  ineq12d  3637  ineqan12d  3638  fnun  5687  undifixp  7563  endisj  7664  sbthlem8  7694  fiin  7941  pm54.43  8439  kmlem9  8593  indistopon  20028  epttop  20036  restbas  20186  ordtbas2  20219  txbas  20594  ptbasin  20604  trfbas2  20870  snfil  20891  fbasrn  20911  trfil2  20914  fmfnfmlem3  20983  ustuqtop2  21269  minveclem3b  22382  minveclem3bOLD  22394  isperp  24769  frrlem4  30529  diophin  35627  kelac2lem  35934