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  6429  mulnq0mo  6430  prcdnql  6466  prcunqu  6467  prnmaxl  6470  prnminu  6471  genprndl  6504  genprndu  6505  distrlem1prl  6556  distrlem1pru  6557  distrlem5prl  6560  distrlem5pru  6561  recexprlemss1l  6605  recexprlemss1u  6606  addsrmo  6631  mulsrmo  6632  mulgt0sr  6664  ltleletr  6857  mulgt1  7570  fzind  8089  eqreznegel  8285  fzen  8637  elfzodifsumelfzo  8787  bernneq  8982  bj-sbimedh  9180  bj-nnen2lp  9342
  Copyright terms: Public domain W3C validator