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  835  3expib  1106  sbiedh  1667  equs5  1707  moexexdc  1981  rsp2  2365  moi  2718  reu6  2724  sbciegft  2787  prel12  3533  opthpr  3534  invdisj  3750  sowlin  4048  reusv1  4156  relop  4429  elres  4589  iss  4597  funssres  4885  fv3  5140  funfvima  5333  poxp  5794  tfri3  5894  nndi  6004  nnmass  6005  nnmordi  6025  nnmord  6026  eroveu  6133  addnq0mo  6430  mulnq0mo  6431  prcdnql  6467  prcunqu  6468  prnmaxl  6471  prnminu  6472  genprndl  6504  genprndu  6505  distrlem1prl  6558  distrlem1pru  6559  distrlem5prl  6562  distrlem5pru  6563  recexprlemss1l  6607  recexprlemss1u  6608  addsrmo  6671  mulsrmo  6672  mulgt0sr  6704  ltleletr  6897  mulgt1  7610  fzind  8129  eqreznegel  8325  fzen  8677  elfzodifsumelfzo  8827  bernneq  9022  bj-sbimedh  9246  bj-nnen2lp  9414
  Copyright terms: Public domain W3C validator