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

Theorem impexp 261
 Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
Assertion
Ref Expression
impexp

Proof of Theorem impexp
StepHypRef Expression
1 pm3.3 259 . 2
2 pm3.31 260 . 2
31, 2impbii 125 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  imp4a  344  exp4a  361  imdistan  438  pm5.3  464  pm4.87  529  nan  664  pm4.14dc  858  pm5.6dc  894  2sb6  1935  2sb6rf  1941  2exsb  1960  mor  2017  eu2  2019  moanim  2049  r2alf  2427  r3al  2452  r19.23t  2514  ceqsralt  2685  rspc2gv  2773  ralrab  2816  ralrab2  2820  euind  2842  reu2  2843  reu3  2845  rmo4  2848  rmo3f  2852  reuind  2860  rmo2ilem  2968  rmo3  2970  ralss  3131  rabss  3142  raldifb  3184  unissb  3734  elintrab  3751  ssintrab  3762  dftr5  3997  repizf2lem  4053  reusv3  4349  tfi  4464  raliunxp  4648  fununi  5159  dff13  5635  dfsmo2  6150  tfr1onlemaccex  6211  tfrcllemaccex  6224  qliftfun  6477  prime  9104  raluz  9325  raluz2  9326  ralrp  9414  facwordi  10437  modfsummod  11178  isprm2  11705  isprm4  11707  metcnp  12587  limcdifap  12706  bdcriota  12915
 Copyright terms: Public domain W3C validator