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

Theorem 3expib 1167
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expib  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)

Proof of Theorem 3expib
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1163 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 252 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  3anidm12  1256  mob  2837  eqbrrdva  4677  funimaexglem  5174  fco  5256  f1oiso2  5694  caovimo  5930  smoel2  6166  nnaword  6373  3ecoptocl  6484  sbthlemi10  6820  distrnq0  7231  addassnq0  7234  prcdnql  7256  prcunqu  7257  genpdisj  7295  cauappcvgprlemrnd  7422  caucvgprlemrnd  7445  caucvgprprlemrnd  7473  nn0n0n1ge2b  9084  fzind  9120  icoshft  9724  fzen  9774  seq3coll  10536  shftuz  10540  mulgcd  11611  algcvga  11639  lcmneg  11662  blssps  12502  blss  12503  metcnp3  12586
  Copyright terms: Public domain W3C validator