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

Theorem impd 251
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 80 . . 3  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
32imp 122 . 2  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
43com12 30 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem is referenced by:  imp32  253  pm3.31  258  syland  287  imp4c  343  imp4d  344  imp5d  351  expimpd  355  expl  370  pm3.37  826  pm5.6r  874  3expib  1146  sbiedh  1717  equs5  1757  moexexdc  2032  rsp2  2425  moi  2796  reu6  2802  sbciegft  2867  prel12  3610  opthpr  3611  invdisj  3831  sowlin  4138  reusv1  4271  relop  4574  elres  4735  iss  4745  funssres  5042  fv3  5312  funfvima  5508  poxp  5979  tfri3  6114  nndi  6229  nnmass  6230  nnmordi  6255  nnmord  6256  eroveu  6363  suplubti  6674  addnq0mo  6985  mulnq0mo  6986  prcdnql  7022  prcunqu  7023  prnmaxl  7026  prnminu  7027  genprndl  7059  genprndu  7060  distrlem1prl  7120  distrlem1pru  7121  distrlem5prl  7124  distrlem5pru  7125  recexprlemss1l  7173  recexprlemss1u  7174  addsrmo  7268  mulsrmo  7269  mulgt0sr  7302  ltleletr  7546  mulgt1  8296  fzind  8831  eqreznegel  9068  fzen  9426  elfzodifsumelfzo  9577  bernneq  10039  mulcn2  10665  divalglemeunn  11014  divalglemeuneg  11016  ndvdssub  11023  algcvgblem  11124  coprmdvds  11167  coprmdvds2  11168  divgcdcoprm0  11176  bj-sbimedh  11329  bj-nnen2lp  11506
  Copyright terms: Public domain W3C validator