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

Theorem impd 242
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 75 . . 3 (ψ → (χ → (φθ)))
32imp 115 . 2 ((ψ χ) → (φθ))
43com12 27 1 (φ → ((ψ χ) → θ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem is referenced by:  imp32  244  pm3.31  249  syland  277  imp4c  333  imp4d  334  imp5d  341  expimpd  345  expl  360  pm5.6r  824  3expib  1093  sbiedh  1652  equs5  1692  moexexdc  1966  rsp2  2349  moi  2701  reu6  2707  sbciegft  2770  prel12  3516  opthpr  3517  invdisj  3733  sowlin  4031  reusv1  4140  relop  4413  elres  4573  iss  4581  funssres  4868  fv3  5122  funfvima  5315  poxp  5775  tfri3  5875  nndi  5980  nnmass  5981  nnmordi  6000  nnmord  6001  eroveu  6108  addnq0mo  6302  mulnq0mo  6303  prcdnql  6338  prcunqu  6339  prnmaxl  6342  prnminu  6343  genprndl  6376  genprndu  6377  distrlem1prl  6421  distrlem1pru  6422  distrlem5prl  6425  distrlem5pru  6426  recexprlemss1l  6469  recexprlemss1u  6470  addsrmo  6490  mulsrmo  6491  mulgt0sr  6522  ltleletr  6698  bj-sbimedh  7018  bj-nnen2lp  7176
  Copyright terms: Public domain W3C validator