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

Theorem 3impia 1101
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 1098 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
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 887
This theorem is referenced by:  mopick2  1983  3gencl  2588  mob2  2721  moi  2724  reupick3  3222  disjne  3273  tz7.2  4091  funopg  4934  fvun1  5239  fvopab6  5264  isores3  5455  ovmpt4g  5623  ovmpt2s  5624  ov2gf  5625  ofrval  5722  poxp  5853  smoel  5915  nnaass  6064  qsel  6183  xpdom3m  6308  phpm  6327  prarloclem3  6593  aptisr  6861  axpre-apti  6957  axapti  7088  divvalap  7651  letrp1  7812  p1le  7813  zextle  8329  zextlt  8330  btwnnz  8332  gtndiv  8333  uzind2  8348  fzind  8351  iccleub  8798  uzsubsubfz  8909  elfz0fzfz0  8981  difelfznle  8991  elfzo0le  9039  fzonmapblen  9041  fzofzim  9042  fzosplitprm1  9088  qbtwnzlemstep  9101  rebtwn2zlemstep  9105  expcl2lemap  9241  expclzaplem  9253  expnegzap  9263  leexp2r  9282  expnbnd  9346  absexpzap  9650
  Copyright terms: Public domain W3C validator