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

Theorem 3expib 1206
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 1202 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32impd 254 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3anidm12  1295  mob  2919  eqbrrdva  4797  funimaexglem  5299  fco  5381  f1oiso2  5827  caovimo  6067  smoel2  6303  nnaword  6511  3ecoptocl  6623  sbthlemi10  6964  distrnq0  7457  addassnq0  7460  prcdnql  7482  prcunqu  7483  genpdisj  7521  cauappcvgprlemrnd  7648  caucvgprlemrnd  7671  caucvgprprlemrnd  7699  nn0n0n1ge2b  9330  fzind  9366  icoshft  9988  fzen  10040  seq3coll  10817  shftuz  10821  mulgcd  12011  algcvga  12045  lcmneg  12068  isnmgm  12733  iscmnd  13054  unitmulclb  13236  blssps  13820  blss  13821  metcnp3  13904  sincosq1sgn  14140  sincosq2sgn  14141  sincosq3sgn  14142  sincosq4sgn  14143
  Copyright terms: Public domain W3C validator