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

Theorem 3impia 1140
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
3impia  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 113 . 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:  mopick2  2031  3gencl  2653  mob2  2793  moi  2796  reupick3  3282  disjne  3333  disji2  3830  tz7.2  4172  funopg  5034  fvun1  5354  fvopab6  5380  isores3  5576  ovmpt4g  5749  ovmpt2s  5750  ov2gf  5751  ofrval  5848  poxp  5979  smoel  6047  tfr1onlemaccex  6095  tfrcllemaccex  6108  nnaass  6228  qsel  6349  xpdom3m  6530  phpm  6561  prarloclem3  7035  aptisr  7303  axpre-apti  7399  axapti  7536  addn0nid  7831  divvalap  8115  letrp1  8281  p1le  8282  zextle  8807  zextlt  8808  btwnnz  8810  gtndiv  8811  uzind2  8828  fzind  8831  iccleub  9318  uzsubsubfz  9430  elfz0fzfz0  9502  difelfznle  9511  elfzo0le  9561  fzonmapblen  9563  fzofzim  9564  fzosplitprm1  9610  rebtwn2zlemstep  9629  qbtwnxr  9634  expcl2lemap  9932  expclzaplem  9944  expnegzap  9954  leexp2r  9974  expnbnd  10042  bcval4  10125  bccmpl  10127  absexpzap  10478  divalgb  11018  ndvdssub  11023  dvdsgcd  11094  dfgcd2  11096  rplpwr  11109  lcmgcdlem  11152  coprmdvds1  11166  qredeq  11171  prmdvdsexpr  11222
  Copyright terms: Public domain W3C validator