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

Theorem impd 251
Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)
Hypothesis
Ref Expression
imp3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
impd (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem impd
StepHypRef Expression
1 imp3.1 . . . 4 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3l 80 . . 3 (𝜓 → (𝜒 → (𝜑𝜃)))
32imp 122 . 2 ((𝜓𝜒) → (𝜑𝜃))
43com12 30 1 (𝜑 → ((𝜓𝜒) → 𝜃))
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  824  pm5.6r  872  3expib  1144  sbiedh  1714  equs5  1754  moexexdc  2029  rsp2  2421  moi  2789  reu6  2795  sbciegft  2858  prel12  3598  opthpr  3599  invdisj  3815  sowlin  4121  reusv1  4254  relop  4554  elres  4715  iss  4725  funssres  5021  fv3  5291  funfvima  5487  poxp  5954  tfri3  6086  nndi  6201  nnmass  6202  nnmordi  6227  nnmord  6228  eroveu  6335  suplubti  6639  addnq0mo  6950  mulnq0mo  6951  prcdnql  6987  prcunqu  6988  prnmaxl  6991  prnminu  6992  genprndl  7024  genprndu  7025  distrlem1prl  7085  distrlem1pru  7086  distrlem5prl  7089  distrlem5pru  7090  recexprlemss1l  7138  recexprlemss1u  7139  addsrmo  7233  mulsrmo  7234  mulgt0sr  7267  ltleletr  7511  mulgt1  8259  fzind  8794  eqreznegel  9031  fzen  9389  elfzodifsumelfzo  9540  bernneq  9970  mulcn2  10593  divalglemeunn  10796  divalglemeuneg  10798  ndvdssub  10805  algcvgblem  10906  coprmdvds  10949  coprmdvds2  10950  divgcdcoprm0  10958  bj-sbimedh  11110  bj-nnen2lp  11287
  Copyright terms: Public domain W3C validator