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

Theorem impd 254
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 124 . 2 ((𝜓𝜒) → (𝜑𝜃))
43com12 30 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem is referenced by:  impcomd  255  imp32  257  pm3.31  262  syland  293  imp4c  351  imp4d  352  imp5d  359  expimpd  363  expl  378  pm3.37  689  pm5.6r  927  3expib  1206  sbiedh  1787  equs5  1829  moexexdc  2110  rsp2  2527  moi  2920  reu6  2926  sbciegft  2993  prel12  3771  opthpr  3772  invdisj  3997  sowlin  4320  reusv1  4458  relop  4777  elres  4943  iss  4953  funssres  5258  fv3  5538  funfvima  5748  poxp  6232  tfri3  6367  nndi  6486  nnmass  6487  nnmordi  6516  nnmord  6517  eroveu  6625  fiintim  6927  suplubti  6998  addnq0mo  7445  mulnq0mo  7446  prcdnql  7482  prcunqu  7483  prnmaxl  7486  prnminu  7487  genprndl  7519  genprndu  7520  distrlem1prl  7580  distrlem1pru  7581  distrlem5prl  7584  distrlem5pru  7585  recexprlemss1l  7633  recexprlemss1u  7634  addsrmo  7741  mulsrmo  7742  mulgt0sr  7776  ltleletr  8038  mulgt1  8819  fzind  9367  eqreznegel  9613  fzen  10042  elfzodifsumelfzo  10200  bernneq  10640  mulcn2  11319  prodmodclem2  11584  dvdsmod0  11799  divalglemeunn  11925  divalglemeuneg  11927  ndvdssub  11934  algcvgblem  12048  coprmdvds  12091  coprmdvds2  12092  divgcdcoprm0  12100  pceu  12294  dvdsprmpweqnn  12334  oddprmdvds  12351  infpnlem1  12356  imasaddfnlemg  12734  sgrpidmndm  12820  lmss  13682  lmtopcnp  13686  zabsle1  14336  bj-sbimedh  14459  bj-nnen2lp  14642
  Copyright terms: Public domain W3C validator