Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineqan12d Unicode version

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
StepHypRef Expression
1 ineq1d.1 . 2
2 ineqan12d.2 . 2
3 ineq12 3694 . 2
41, 2, 3syl2an 477 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator