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  6595  aptisr  6863  axpre-apti  6959  axapti  7090  divvalap  7653  letrp1  7814  p1le  7815  zextle  8331  zextlt  8332  btwnnz  8334  gtndiv  8335  uzind2  8350  fzind  8353  iccleub  8800  uzsubsubfz  8911  elfz0fzfz0  8983  difelfznle  8993  elfzo0le  9041  fzonmapblen  9043  fzofzim  9044  fzosplitprm1  9090  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  expcl2lemap  9267  expclzaplem  9279  expnegzap  9289  leexp2r  9308  expnbnd  9372  absexpzap  9676
 Copyright terms: Public domain W3C validator