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

Theorem 3impia 1112
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 112 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1109 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  mopick2  1999  3gencl  2605  mob2  2743  moi  2746  reupick3  3249  disjne  3300  tz7.2  4118  funopg  4961  fvun1  5266  fvopab6  5291  isores3  5482  ovmpt4g  5650  ovmpt2s  5651  ov2gf  5652  ofrval  5749  poxp  5880  smoel  5945  nnaass  6094  qsel  6213  xpdom3m  6338  phpm  6357  prarloclem3  6652  aptisr  6920  axpre-apti  7016  axapti  7148  addn0nid  7443  divvalap  7726  letrp1  7888  p1le  7889  zextle  8388  zextlt  8389  btwnnz  8391  gtndiv  8392  uzind2  8408  fzind  8411  iccleub  8900  uzsubsubfz  9012  elfz0fzfz0  9084  difelfznle  9094  elfzo0le  9142  fzonmapblen  9144  fzofzim  9145  fzosplitprm1  9191  qbtwnzlemstep  9204  rebtwn2zlemstep  9208  expcl2lemap  9426  expclzaplem  9438  expnegzap  9448  leexp2r  9468  expnbnd  9533  bcval4  9613  bccmpl  9615  absexpzap  9899
  Copyright terms: Public domain W3C validator