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

Theorem 3expib 1147
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expib (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem 3expib
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1143 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 252 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 927
This theorem is referenced by:  3anidm12  1232  mob  2798  eqbrrdva  4619  funimaexglem  5110  fco  5189  f1oiso2  5620  caovimo  5852  smoel2  6082  nnaword  6284  3ecoptocl  6395  sbthlemi10  6729  distrnq0  7072  addassnq0  7075  prcdnql  7097  prcunqu  7098  genpdisj  7136  cauappcvgprlemrnd  7263  caucvgprlemrnd  7286  caucvgprprlemrnd  7314  nn0n0n1ge2b  8880  fzind  8915  icoshft  9461  fzen  9511  iseqcoll  10301  shftuz  10305  mulgcd  11337  algcvga  11365  lcmneg  11388
  Copyright terms: Public domain W3C validator