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

Theorem 3impib 1201
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 258 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1193 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  mob  2919  eqreu  2929  iotam  5208  funimaexglem  5299  ssimaexg  5578  rbropap  6243  dfsmo2  6287  3ecoptocl  6623  distrnq0  7457  addassnq0  7460  uzind  9362  fzind  9366  fnn0ind  9367  xltnegi  9833  facwordi  10715  shftvalg  10840  shftval4g  10841  mulgcd  12011  coprmdvds1  12085  pcfac  12342  mgmcl  12772  mhmlin  12852  mhmmulg  13017  issubg2m  13042  nsgbi  13057  srgmulgass  13165  dvdsrtr  13263  issubrg2  13362  inopn  13434  basis1  13478  cnmpt2t  13724  cnmpt22  13725  cnmptcom  13729  xmeteq0  13790  sincosq1sgn  14178  sincosq2sgn  14179  sincosq3sgn  14180  sincosq4sgn  14181  speano5  14616
  Copyright terms: Public domain W3C validator