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

Theorem impd 254
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
impd  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem impd
StepHypRef Expression
1 imp3.1 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3l 81 . . 3  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
32imp 124 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 30 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem is referenced by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  690  pm5.6r  928  3expib  1208  sbiedh  1798  equs5  1840  moexexdc  2122  rsp2  2540  moi  2935  reu6  2941  sbciegft  3008  prel12  3789  opthpr  3790  invdisj  4015  sowlin  4341  reusv1  4479  relop  4798  elres  4964  iss  4974  funssres  5280  fv3  5560  funfvima  5772  poxp  6261  tfri3  6396  nndi  6515  nnmass  6516  nnmordi  6545  nnmord  6546  eroveu  6656  fiintim  6961  suplubti  7033  addnq0mo  7481  mulnq0mo  7482  prcdnql  7518  prcunqu  7519  prnmaxl  7522  prnminu  7523  genprndl  7555  genprndu  7556  distrlem1prl  7616  distrlem1pru  7617  distrlem5prl  7620  distrlem5pru  7621  recexprlemss1l  7669  recexprlemss1u  7670  addsrmo  7777  mulsrmo  7778  mulgt0sr  7812  ltleletr  8074  mulgt1  8855  fzind  9403  eqreznegel  9650  fzen  10079  elfzodifsumelfzo  10237  bernneq  10681  mulcn2  11361  prodmodclem2  11626  dvdsmod0  11841  divalglemeunn  11967  divalglemeuneg  11969  ndvdssub  11976  algcvgblem  12092  coprmdvds  12135  coprmdvds2  12136  divgcdcoprm0  12144  pceu  12338  dvdsprmpweqnn  12379  oddprmdvds  12397  infpnlem1  12402  imasaddfnlemg  12802  sgrpidmndm  12904  imasabl  13298  lmss  14231  lmtopcnp  14235  zabsle1  14886  bj-sbimedh  15009  bj-nnen2lp  15192
  Copyright terms: Public domain W3C validator