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

Theorem 3impib 1137
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 1133 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 920
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 922
This theorem is referenced by:  mob  2784  eqreu  2794  funimaexglem  5034  ssimaexg  5288  dfsmo2  5957  3ecoptocl  6283  distrnq0  6747  addassnq0  6750  uzind  8575  fzind  8579  fnn0ind  8580  xltnegi  9014  facwordi  9800  shftvalg  9909  shftval4g  9910  mulgcd  10596  coprmdvds1  10664  speano5  10990
  Copyright terms: Public domain W3C validator