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

Theorem 3impia 1100
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1
Assertion
Ref Expression
3impia

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3
21ex 108 . 2
323imp 1097 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  mopick2  1980  3gencl  2582  mob2  2715  moi  2718  reupick3  3216  disjne  3267  funopg  4877  fvun1  5182  fvopab6  5207  isores3  5398  ovmpt4g  5565  ovmpt2s  5566  ov2gf  5567  ofrval  5664  poxp  5794  smoel  5856  nnaass  6003  qsel  6119  xpdom3m  6244  prarloclem3  6480  aptisr  6705  axpre-apti  6769  axapti  6887  divvalap  7435  letrp1  7595  p1le  7596  zextle  8107  zextlt  8108  btwnnz  8110  gtndiv  8111  uzind2  8126  fzind  8129  iccleub  8570  uzsubsubfz  8681  elfz0fzfz0  8753  difelfznle  8763  elfzo0le  8811  fzonmapblen  8813  fzofzim  8814  fzosplitprm1  8860  expcl2lemap  8921  expclzaplem  8933  expnegzap  8943  leexp2r  8962  expnbnd  9025
  Copyright terms: Public domain W3C validator