Theorem ineq12 3694

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

Assertion

Ref	Expression
ineq12

Proof of Theorem ineq12

Step	Hyp	Ref	Expression
1		ineq1 3692	. 2
2		ineq2 3693	. 2
3	1, 2	sylan9eq 2518	1

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

This theorem is referenced by:  ineq12i  3697  ineq12d  3700  ineqan12d  3701  fnun  5692  undifixp  7525  endisj  7624  sbthlem8  7654  fiin  7902  pm54.43  8402  kmlem9  8559  indistopon  19502  epttop  19510  restbas  19659  ordtbas2  19692  txbas  20068  ptbasin  20078  trfbas2  20344  snfil  20365  fbasrn  20385  trfil2  20388  fmfnfmlem3  20457  ustuqtop2  20745  minveclem3b  21843  isperp  24089  frrlem4  29390  diophin  30706  kelac2lem  31010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482