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

Theorem 3impib 1141
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 254 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1137 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  mob  2797  eqreu  2807  funimaexglem  5097  ssimaexg  5366  dfsmo2  6052  3ecoptocl  6381  distrnq0  7018  addassnq0  7021  uzind  8857  fzind  8861  fnn0ind  8862  xltnegi  9297  facwordi  10148  shftvalg  10270  shftval4g  10271  mulgcd  11283  coprmdvds1  11351  inopn  11600  speano5  11839
  Copyright terms: Public domain W3C validator