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

Theorem 3impia 1161
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 114 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1158 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  mopick2  2058  3gencl  2692  mob2  2835  moi  2838  reupick3  3329  disjne  3384  disji2  3890  tz7.2  4244  funopg  5125  fvun1  5453  fvopab6  5483  isores3  5682  ovmpt4g  5859  ovmpos  5860  ov2gf  5861  ofrval  5958  poxp  6095  smoel  6163  tfr1onlemaccex  6211  tfrcllemaccex  6224  nnaass  6347  qsel  6472  xpdom3m  6694  phpm  6725  ctssdc  6964  mkvprop  6998  prarloclem3  7269  aptisr  7551  axpre-apti  7657  axapti  7799  addn0nid  8100  divvalap  8397  letrp1  8566  p1le  8567  zextle  9096  zextlt  9097  btwnnz  9099  gtndiv  9100  uzind2  9117  fzind  9120  iccleub  9665  uzsubsubfz  9778  elfz0fzfz0  9854  difelfznle  9863  elfzo0le  9913  fzonmapblen  9915  fzofzim  9916  fzosplitprm1  9962  rebtwn2zlemstep  9981  qbtwnxr  9986  expcl2lemap  10256  expclzaplem  10268  expnegzap  10278  leexp2r  10298  expnbnd  10366  bcval4  10449  bccmpl  10451  absexpzap  10803  divalgb  11529  ndvdssub  11534  dvdsgcd  11607  dfgcd2  11609  rplpwr  11622  lcmgcdlem  11665  coprmdvds1  11679  qredeq  11684  prmdvdsexpr  11735  elrestr  12034  mopni  12557
  Copyright terms: Public domain W3C validator