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

Theorem 3impib 1183
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 1176 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963
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 965
This theorem is referenced by:  mob  2894  eqreu  2904  funimaexglem  5253  ssimaexg  5530  rbropap  6190  dfsmo2  6234  3ecoptocl  6569  distrnq0  7379  addassnq0  7382  uzind  9275  fzind  9279  fnn0ind  9280  xltnegi  9739  facwordi  10614  shftvalg  10736  shftval4g  10737  mulgcd  11900  coprmdvds1  11968  inopn  12412  basis1  12456  cnmpt2t  12704  cnmpt22  12705  cnmptcom  12709  xmeteq0  12770  sincosq1sgn  13158  sincosq2sgn  13159  sincosq3sgn  13160  sincosq4sgn  13161  speano5  13530
  Copyright terms: Public domain W3C validator