Theorem ineq12d 3700

Description: Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
ineq1d.1
ineq12d.2

Assertion

Ref	Expression
ineq12d

Proof of Theorem ineq12d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2
2		ineq12d.2	. 2
3		ineq12 3694	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  ->wi 4  =wceq 1395  i^icin 3474

This theorem is referenced by:  csbin  3860  csbingOLD  3861  funprg  5642  funtpg  5643  offval  6547  ofrfval  6548  oev2  7192  isf32lem7  8760  ressval  14684  invffval  15152  invfval  15153  oppcinv  15170  isps  15832  dmdprd  17029  dprddisj  17042  dprdf1o  17079  dmdprdsplit2lem  17094  dmdprdpr  17098  pgpfaclem1  17132  isunit  17306  dfrhm2  17366  isrhm  17370  2idlval  17881  aspval  17977  ressmplbas2  18117  pjfval  18737  iscon  19914  consuba  19921  ptbasin  20078  ptclsg  20116  qtopval  20196  rnelfmlem  20453  trust  20732  isnmhm  21253  uniioombllem2a  21991  dyaddisjlem  22004  dyaddisj  22005  i1faddlem  22100  i1fmullem  22101  limcflf  22285  ispth  24570  1pthonlem2  24592  2pthlem2  24598  constr2pth  24603  constr3pthlem3  24657  frisusgranb  24997  2spotdisj  25061  chocin  26413  cmbr3  26526  pjoml3  26530  fh1  26536  xppreima2  27488  hauseqcn  27877  prsssdm  27899  ordtrestNEW  27903  ordtrest2NEW  27905  cndprobval  28372  ballotlemfrc  28465  msrval  28898  msrf  28902  ismfs  28909  predeq123  29245  itg2addnclem2  30067  clsun  30146  heiborlem4  30310  heiborlem6  30312  heiborlem10  30316  aomclem8  31007  dvsinax  31708  dvcosax  31723  usgra2pthspth  32351  isofn  32567  dfiso2  32568  zerooval  32605  rhmval  32725  bnj1421  34098  pmodl42N  35575  polfvalN  35628  poldmj1N  35652  pmapj2N  35653  pnonsingN  35657  psubclinN  35672  poml4N  35677  osumcllem9N  35688  trnfsetN  35880  diainN  36784  djaffvalN  36860  djafvalN  36861  djajN  36864  dihmeetcl  37072  dihmeet2  37073  dochnoncon  37118  djhffval  37123  djhfval  37124  djhlj  37128  dochdmm1  37137  lclkrlem2g  37240  lclkrlem2v  37255  lcfrlem21  37290  lcfrlem24  37293  mapdunirnN  37377  baerlem5amN  37443  baerlem5bmN  37444  baerlem5abmN  37445  mapdheq4lem  37458  mapdh6lem1N  37460  mapdh6lem2N  37461  hdmap1l6lem1  37535  hdmap1l6lem2  37536

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