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

Theorem 3impb 1086
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impb.1 ((φ (ψ χ)) → θ)
Assertion
Ref Expression
3impb ((φ ψ χ) → θ)

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3 ((φ (ψ χ)) → θ)
21exp32 347 . 2 (φ → (ψ → (χθ)))
323imp 1084 1 ((φ ψ χ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 873
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 875
This theorem is referenced by:  3adant1l  1113  3adant1r  1114  3impdi  1176  vtocl3gf  2593  rspc2ev  2641  reuss  3195  trssord  4066  funtp  4878  resdif  5073  funimass4  5149  fnovex  5462  fnotovb  5471  fovrn  5566  fnovrn  5571  fmpt2co  5760  nndi  5980  nnaordi  5992  ecovass  6126  ecoviass  6127  ecovdi  6128  ecovidi  6129  addasspig  6190  mulasspig  6192  distrpig  6193  distrnq0  6314  addassnq0  6317  distnq0r  6318  prcdnql  6338  prcunqu  6339  genpassl  6379  genpassu  6380  genpassg  6381  distrlem1prl  6421  distrlem1pru  6422  ltexprlemopl  6438  ltexprlemopu  6440  cnegexlem1  6773  subadd  6801  addsub  6809  subdi  6968  submul2  6982
  Copyright terms: Public domain W3C validator