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

Theorem impd 252
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 81 . . 3 (𝜓 → (𝜒 → (𝜑𝜃)))
32imp 123 . 2 ((𝜓𝜒) → (𝜑𝜃))
43com12 30 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem is referenced by:  impcomd  253  imp32  255  pm3.31  260  syland  291  imp4c  348  imp4d  349  imp5d  356  expimpd  360  expl  375  pm3.37  678  pm5.6r  912  3expib  1184  sbiedh  1760  equs5  1801  moexexdc  2083  rsp2  2482  moi  2867  reu6  2873  sbciegft  2939  prel12  3698  opthpr  3699  invdisj  3923  sowlin  4242  reusv1  4379  relop  4689  elres  4855  iss  4865  funssres  5165  fv3  5444  funfvima  5649  poxp  6129  tfri3  6264  nndi  6382  nnmass  6383  nnmordi  6412  nnmord  6413  eroveu  6520  fiintim  6817  suplubti  6887  addnq0mo  7262  mulnq0mo  7263  prcdnql  7299  prcunqu  7300  prnmaxl  7303  prnminu  7304  genprndl  7336  genprndu  7337  distrlem1prl  7397  distrlem1pru  7398  distrlem5prl  7401  distrlem5pru  7402  recexprlemss1l  7450  recexprlemss1u  7451  addsrmo  7558  mulsrmo  7559  mulgt0sr  7593  ltleletr  7853  mulgt1  8628  fzind  9173  eqreznegel  9413  fzen  9830  elfzodifsumelfzo  9985  bernneq  10419  mulcn2  11088  prodmodclem2  11353  divalglemeunn  11625  divalglemeuneg  11627  ndvdssub  11634  algcvgblem  11737  coprmdvds  11780  coprmdvds2  11781  divgcdcoprm0  11789  lmss  12425  lmtopcnp  12429  bj-sbimedh  13008  bj-nnen2lp  13182
  Copyright terms: Public domain W3C validator