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

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

Proof of Theorem excom
StepHypRef Expression
1 excomim 1535 . 2 (xyφyxφ)
2 excomim 1535 . 2 (yxφxyφ)
31, 2impbii 117 1 (xyφyxφ)
Colors of variables: wff set class
Syntax hints:  wb 98  wex 1362
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 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-ial 1409
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  excom13  1561  exrot3  1562  ee4anv  1791  sbexyz  1861  2exsb  1867  2euex  1969  2exeu  1974  2eu4  1975  rexcomf  2450  gencbvex  2577  euxfr2dc  2703  euind  2705  sbccomlem  2809  opelopabsbALT  3970  uniuni  4133  elvvv  4330  dmuni  4472  dm0rn0  4479  dmmrnm  4481  dmcosseq  4530  elres  4573  rnco  4754  coass  4766  oprabid  5461  dfoprab2  5475  opabex3d  5671  opabex3  5672  prarloc  6357
  Copyright terms: Public domain W3C validator