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

Theorem 3impia 1136
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 1133 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 920
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 922
This theorem is referenced by:  mopick2  2026  3gencl  2642  mob2  2782  moi  2785  reupick3  3266  disjne  3314  tz7.2  4138  funopg  4985  fvun1  5292  fvopab6  5317  isores3  5507  ovmpt4g  5675  ovmpt2s  5676  ov2gf  5677  ofrval  5774  poxp  5905  smoel  5970  tfr1onlemaccex  6018  tfrcllemaccex  6031  nnaass  6150  qsel  6271  xpdom3m  6400  phpm  6422  prarloclem3  6785  aptisr  7053  axpre-apti  7149  axapti  7286  addn0nid  7581  divvalap  7865  letrp1  8029  p1le  8030  zextle  8555  zextlt  8556  btwnnz  8558  gtndiv  8559  uzind2  8576  fzind  8579  iccleub  9066  uzsubsubfz  9178  elfz0fzfz0  9250  difelfznle  9259  elfzo0le  9307  fzonmapblen  9309  fzofzim  9310  fzosplitprm1  9356  rebtwn2zlemstep  9375  qbtwnxr  9380  expcl2lemap  9621  expclzaplem  9633  expnegzap  9643  leexp2r  9663  expnbnd  9729  bcval4  9812  bccmpl  9814  absexpzap  10151  divalgb  10516  ndvdssub  10521  dvdsgcd  10592  dfgcd2  10594  rplpwr  10607  lcmgcdlem  10650  coprmdvds1  10664  qredeq  10669  prmdvdsexpr  10720
  Copyright terms: Public domain W3C validator