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

Theorem 3impib 1162
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impib.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
3impib  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impib
StepHypRef Expression
1 3impib.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21expd 256 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1158 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:  mob  2837  eqreu  2847  funimaexglem  5174  ssimaexg  5449  rbropap  6106  dfsmo2  6150  3ecoptocl  6484  distrnq0  7231  addassnq0  7234  uzind  9113  fzind  9117  fnn0ind  9118  xltnegi  9558  facwordi  10426  shftvalg  10548  shftval4g  10549  mulgcd  11600  coprmdvds1  11668  inopn  12065  basis1  12109  cnmpt2t  12357  cnmpt22  12358  cnmptcom  12362  xmeteq0  12423  speano5  12953
  Copyright terms: Public domain W3C validator