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

Theorem 3impib 1196
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 1188 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 973
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 975
This theorem is referenced by:  mob  2912  eqreu  2922  iotam  5190  funimaexglem  5281  ssimaexg  5558  rbropap  6222  dfsmo2  6266  3ecoptocl  6602  distrnq0  7421  addassnq0  7424  uzind  9323  fzind  9327  fnn0ind  9328  xltnegi  9792  facwordi  10674  shftvalg  10800  shftval4g  10801  mulgcd  11971  coprmdvds1  12045  pcfac  12302  mgmcl  12613  mhmlin  12690  inopn  12795  basis1  12839  cnmpt2t  13087  cnmpt22  13088  cnmptcom  13092  xmeteq0  13153  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  speano5  13979
  Copyright terms: Public domain W3C validator