ILE Home 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  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )

Proof of Theorem impexp
StepHypRef Expression
1 pm3.3 259 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 260 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 125 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
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  346  exp4a  363  imdistan  440  pm5.3  466  pm4.87  531  nan  666  pm4.14dc  860  pm5.6dc  896  2sb6  1937  2sb6rf  1943  2exsb  1962  mor  2019  eu2  2021  moanim  2051  r2alf  2429  r3al  2454  r19.23t  2516  ceqsralt  2687  rspc2gv  2775  ralrab  2818  ralrab2  2822  euind  2844  reu2  2845  reu3  2847  rmo4  2850  rmo3f  2854  reuind  2862  rmo2ilem  2970  rmo3  2972  ralss  3133  rabss  3144  raldifb  3186  unissb  3736  elintrab  3753  ssintrab  3764  dftr5  3999  repizf2lem  4055  reusv3  4351  tfi  4466  raliunxp  4650  fununi  5161  dff13  5637  dfsmo2  6152  tfr1onlemaccex  6213  tfrcllemaccex  6226  qliftfun  6479  prime  9118  raluz  9341  raluz2  9342  ralrp  9431  facwordi  10454  modfsummod  11195  isprm2  11725  isprm4  11727  metcnp  12608  limcdifap  12727  bdcriota  13008
  Copyright terms: Public domain W3C validator