ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3impia Structured version   GIF 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  6479  aptisr  6685  axpre-apti  6749  axapti  6867  divvalap  7415  letrp1  7575  p1le  7576  zextle  8087  zextlt  8088  btwnnz  8090  gtndiv  8091  uzind2  8106  fzind  8109  iccleub  8550  uzsubsubfz  8661  elfz0fzfz0  8733  difelfznle  8743  elfzo0le  8791  fzonmapblen  8793  fzofzim  8794  fzosplitprm1  8840  expcl2lemap  8901  expclzaplem  8913  expnegzap  8923  leexp2r  8942  expnbnd  9005
  Copyright terms: Public domain W3C validator