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  689  pm5.6r  927  3expib  1206  sbiedh  1787  equs5  1829  moexexdc  2110  rsp2  2527  moi  2920  reu6  2926  sbciegft  2993  prel12  3769  opthpr  3770  invdisj  3994  sowlin  4316  reusv1  4454  relop  4772  elres  4938  iss  4948  funssres  5253  fv3  5533  funfvima  5742  poxp  6226  tfri3  6361  nndi  6480  nnmass  6481  nnmordi  6510  nnmord  6511  eroveu  6619  fiintim  6921  suplubti  6992  addnq0mo  7424  mulnq0mo  7425  prcdnql  7461  prcunqu  7462  prnmaxl  7465  prnminu  7466  genprndl  7498  genprndu  7499  distrlem1prl  7559  distrlem1pru  7560  distrlem5prl  7563  distrlem5pru  7564  recexprlemss1l  7612  recexprlemss1u  7613  addsrmo  7720  mulsrmo  7721  mulgt0sr  7755  ltleletr  8016  mulgt1  8796  fzind  9344  eqreznegel  9590  fzen  10016  elfzodifsumelfzo  10174  bernneq  10613  mulcn2  11291  prodmodclem2  11556  dvdsmod0  11771  divalglemeunn  11896  divalglemeuneg  11898  ndvdssub  11905  algcvgblem  12019  coprmdvds  12062  coprmdvds2  12063  divgcdcoprm0  12071  pceu  12265  dvdsprmpweqnn  12305  oddprmdvds  12322  infpnlem1  12327  sgrpidmndm  12700  lmss  13379  lmtopcnp  13383  zabsle1  14033  bj-sbimedh  14145  bj-nnen2lp  14328
  Copyright terms: Public domain W3C validator