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

Theorem impexp 259
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 257 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 258 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 124 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imp4a  341  exp4a  358  imdistan  433  pm5.3  459  pm4.87  524  nan  661  pm4.14dc  825  pm5.6dc  873  2sb6  1908  2sb6rf  1914  2exsb  1933  mor  1990  eu2  1992  moanim  2022  r2alf  2395  r3al  2420  r19.23t  2479  ceqsralt  2646  rspc2gv  2732  ralrab  2774  ralrab2  2778  euind  2800  reu2  2801  reu3  2803  rmo4  2806  rmo3f  2810  reuind  2818  rmo2ilem  2926  rmo3  2928  ralss  3085  rabss  3096  raldifb  3138  unissb  3678  elintrab  3695  ssintrab  3706  dftr5  3931  repizf2lem  3988  reusv3  4273  tfi  4387  raliunxp  4565  fununi  5068  dff13  5529  dfsmo2  6034  tfr1onlemaccex  6095  tfrcllemaccex  6108  qliftfun  6354  prime  8815  raluz  9035  raluz2  9036  ralrp  9124  facwordi  10113  modfsummod  10815  isprm2  11181  isprm4  11183  bdcriota  11420
  Copyright terms: Public domain W3C validator