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

Theorem 3impia 1112
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 112 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1109 1 ((𝜑𝜓𝜒) → 𝜃)
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  2744  moi  2747  reupick3  3250  disjne  3301  tz7.2  4119  funopg  4962  fvun1  5267  fvopab6  5292  isores3  5483  ovmpt4g  5651  ovmpt2s  5652  ov2gf  5653  ofrval  5750  poxp  5881  smoel  5946  nnaass  6095  qsel  6214  xpdom3m  6339  phpm  6358  prarloclem3  6653  aptisr  6921  axpre-apti  7017  axapti  7149  addn0nid  7444  divvalap  7727  letrp1  7889  p1le  7890  zextle  8389  zextlt  8390  btwnnz  8392  gtndiv  8393  uzind2  8409  fzind  8412  iccleub  8901  uzsubsubfz  9013  elfz0fzfz0  9085  difelfznle  9095  elfzo0le  9143  fzonmapblen  9145  fzofzim  9146  fzosplitprm1  9192  qbtwnzlemstep  9205  rebtwn2zlemstep  9209  qbtwnxr  9214  expcl2lemap  9432  expclzaplem  9444  expnegzap  9454  leexp2r  9474  expnbnd  9540  bcval4  9620  bccmpl  9622  absexpzap  9907  divalgb  10237  ndvdssub  10242
  Copyright terms: Public domain W3C validator