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

Theorem excom 1551
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
excom

Proof of Theorem excom
StepHypRef Expression
1 excomim 1550 . 2
2 excomim 1550 . 2
31, 2impbii 117 1
Colors of variables: wff set class
Syntax hints:   wb 98  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  excom13  1576  exrot3  1577  ee4anv  1806  sbexyz  1876  2exsb  1882  2euex  1984  2exeu  1989  2eu4  1990  rexcomf  2466  gencbvex  2594  euxfr2dc  2720  euind  2722  sbccomlem  2826  opelopabsbALT  3987  uniuni  4149  elvvv  4346  dmuni  4488  dm0rn0  4495  dmmrnm  4497  dmcosseq  4546  elres  4589  rnco  4770  coass  4782  oprabid  5480  dfoprab2  5494  opabex3d  5690  opabex3  5691  domen  6168  xpassen  6240  prarloc  6485
  Copyright terms: Public domain W3C validator