Theorem ineqan12d 3701

Description: Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)

Hypotheses

Ref	Expression
ineq1d.1
ineqan12d.2

Assertion

Ref	Expression
ineqan12d

Proof of Theorem ineqan12d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2
2		ineqan12d.2	. 2
3		ineq12 3694	. 2
4	1, 2, 3	syl2an 477	1

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

This theorem is referenced by:  fvun1  5944  fndmin  5994  offval  6547  ofrfval  6548  offval3  6794  fpar  6904  fisn  7907  ixxin  11575  vdwmc  14496  fvcosymgeq  16454  cssincl  18719  inmbl  21952  iundisj2  21959  itg1addlem3  22105  fh1  26536  iundisj2f  27449  iundisj2fi  27602  wfrlem4  29346

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