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

Theorem 3expib 1106
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3expib (φ → ((ψ χ) → θ))

Proof of Theorem 3expib
StepHypRef Expression
1 3exp.1 . . 3 ((φ ψ χ) → θ)
213exp 1102 . 2 (φ → (ψ → (χθ)))
32impd 242 1 (φ → ((ψ χ) → θ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
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 886
This theorem is referenced by:  3anidm12  1191  mob  2717  eqbrrdva  4448  funimaexglem  4925  fco  4999  f1oiso2  5409  caovimo  5636  smoel2  5859  nnaword  6020  3ecoptocl  6131  distrnq0  6441  addassnq0  6444  prcdnql  6466  prcunqu  6467  genpdisj  6505  cauappcvgprlemrnd  6621  nn0n0n1ge2b  8076  fzind  8109  icoshft  8608  fzen  8657
  Copyright terms: Public domain W3C validator