Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ineq2d Unicode version

Theorem ineq2d 3304
 Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
ineq1d.1
Assertion
Ref Expression
ineq2d

Proof of Theorem ineq2d
StepHypRef Expression
1 ineq1d.1 . 2
2 ineq2 3298 . 2
31, 2syl 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1332   cin 3097 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-v 2711  df-in 3104 This theorem is referenced by:  disjpr2  3619  rint0  3842  riin0  3916  disji2  3954  xpriindim  4717  riinint  4840  reseq2  4854  csbresg  4862  resindm  4901  isoselem  5761  zfz1isolem1  10688  fsumm1  11290  ennnfonelemhf1o  12093  restval  12296  basis1  12384  baspartn  12387  eltg  12391  tgdom  12411  ntrval  12449  resttopon2  12517  restopnb  12520  qtopbasss  12860
 Copyright terms: Public domain W3C validator